David,
Thanks. That all makes sense. The ProofPower read-eval-print loop lives in this executable:
-rwxr-xr-x 1 rda staff 9975056 Jul 25 14:00 /usr/local/pp/latest/bin/pp-ml
and when you add its size to the size of the saved state you get about the same size as the executable. Fortunately, the size of the executable doesn?t seem to be causing any problems in practice (and why should it? A lot of the apps on my phone are much bigger than this, so Poly/ML is competitive with Java on this score :-)).
Regards,
Rob.
On 26 Nov 2021, at 08:38, David Matthews <David.Matthews at prolingua.co.uk> wrote:
Rob,
On 25/11/2021 19:26, Rob Arthan wrote:
-rw-r--r-- 1 rda staff 44217560 Nov 25 19:06 main1.o -rwxr-xr-x 1 rda staff 33928480 Nov 25 19:07 main1 -rw-r--r-- 1 rda staff 24260472 Nov 25 19:10 saved_state Here main1.o is the result of calling PolyML.export, main1 is the executable and saved_state is the result of calling PolyML.Compiler.saveState. He is seeing even bigger differences (possibly because he is compiling on Windows?). The question remains though: why is the .o file much bigger than the executable and why is the executable much bigger than the saved state? Can we do anything to reduce the size of the executable. (We are both calling PolyML.shareCommonData on the entry point function beforecalling PolyML.export.)
Those figures don't surprise me. The saved state contains data created in the session but because it can only be read into the same executable that created it, it doesn't contain anything present in the executable itself.
PolyML.export produces an object file containing everything that is reachable from the root. It will almost certainly contain portions of the original executable so that the resulting code is self-contained.
The object file (main1.o) contains relocation information needed by the linker. If the root includes ML data structures such as lists there will be a lot of relocation data and that could easily double the size of the file. The size and format of the relocation data depend on the platform so are different in Windows, Linux/BSD and Mac OS. The linker may or may not remove this in the final executable. If the executable is linked to be loaded at a fixed address it doesn't need the relocation information.
David