These days I build Poly/ML with all combinations of yes/no for the following configure options for testing purposes: --enable-shared --enable-compact32bit --enable-intinf-as-int

I've just built ProofPower with each such variant of Poly/ML 5.9 on my Linux x86_64 system and get the following sizes for pp-ml:

10485336 pp/bin/pp-ml 10572216 pp--intinf-as-int/bin/pp-ml 8465368 pp--compact32bit/bin/pp-ml 8547736 pp--compact32bit--intinf-as-int/bin/pp-ml 9795648 pp--shared/bin/pp-ml 9882528 pp--shared--intinf-as-int/bin/pp-ml 7767840 pp--shared--compact32bit/bin/pp-ml 7846104 pp--shared--compact32bit--intinf-as-int/bin/pp-ml

and the following sizes for a saved state (zed.polydb):

18650832 pp/db/zed.polydb 18802280 pp--intinf-as-int/db/zed.polydb 14424536 pp--compact32bit/db/zed.polydb 14610524 pp--compact32bit--intinf-as-int/db/zed.polydb 18650616 pp--shared/db/zed.polydb 18802744 pp--shared--intinf-as-int/db/zed.polydb 14424356 pp--shared--compact32bit/db/zed.polydb 14610524 pp--shared--compact32bit--intinf-as-int/db/zed.polydb

Using compact32bit gives a significant reduction in file size of both pp-ml and saved states. Dynamically linking to libpolyml reduces the size of pp-ml by 690-700 kB versus static linking but does not affect the size of saved states, as you would expect. Not using intinf-as-int reduces file sizes by around 1%.

So building ProofPower on a Poly/ML built using compact32bit, dynamic linking and not using intinf-as-int would help minimize file sizes.

Phil

On 27/11/21 00:10, Rob Arthan wrote:

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

---

polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml