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.matth...@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@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
