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 > <[email protected]> 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
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
