Hi David,
the short answer is, comparing with 5.7.1 release, both the latest master and the 32-in-64 option make the difference, but actually not that big as I reported yesterday.
Here are the test steps (of each round):
1. I do a full build of HOL4 in my working branch (in which the probability theories are greatly changed, also with one single theorem of 1500 lines of scripts). 2. I touched a base file (util_probScript.sml) in HOL?s ?src/probability?, then re-do the incremental build using single processor (but without generating theory html files at the end), thus all computation were used on compiling proof scripts in ?src/probability?.
I used Unix ?time? command to record the ?real" time spent on step 2, using three PolyML versions: 1) 5.7.1 release, 2) latest master (x64), 3) latest master (32-in-64). All tests were repeated 3 times, then I take the average time as the calculating basis. Below is the record:
[1] Poly/ML 5.7.1 Release 2m13.589s (133.589s) 2m11.944s (131.944s) 2m12.155s (132.155s) (average: 132.563s)
[2] Poly/ML 5.7.1 Release (Git version v5.7.1-481-g0a6ebca4) 2m11.569s (131.569s) 2m9.437s (129.437s) 2m9.820s (129.820s) (average: 130.275s)
[3] Poly/ML 5.7.1 32-in-64 (Git version v5.7.1-481-g0a6ebca4) 2m6.087s (126.087s) 2m7.180s (127.180s) 2m7.077s (127.077s) (average: 126.781s)
Thus, from 5.7.1 release to latest master (x64), I observed about 1.7% performance increments; from latest master (x64) to latest master (32-in-64), I observed another 2.7% performance increments; in total, from 5.7.1 release to latest master (32-in-64) there?re about 4.3% performance increments.
My observation yesterday (10%) was based on the time spent on the best single proof script. But actually from one version of PolyML to another, not all proof scripts get compiled faster. But I believe the total time spent on building the whole HOL4 should follow the same trends.
P. S. I think PolyML is already fast enough for HOL4, especially when you see how slow the Moscow ML builds are:) In Isabelle, every time when the user click inside the JEdit editor, it may trigger some computation at the PolyML side, I guess the performance issue is more urgent there.
Hope this helps,
Chun
Il giorno 22 gen 2019, alle ore 23:53, David Matthews <David.Matthews at prolingua.co.uk> ha scritto:
Thanks, that's interesting. Have you tried the latest master with native 64-bits? It would be useful to know whether it's the 32-in-64 that makes the difference for HOL4 or the changes to the code-generator.
Regards, David
On 22/01/2019 11:42, Chun Tian (binghe) wrote:
I observed about 10% performance improvements in HOL4, between 5.7.1 release (x86_64) and latest master with the --enable-compact32bit option. ?Chun