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