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