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

Reply via email to