16 Jun
2020
16 Jun
'20
2:30 a.m.
I have some HOL code that runs to completion in ~24 seconds user time.
On 5.7.1 it runs in about that much wall clock time too. (Unfortunately, this test is running on a different machine, necessarily, but this is an old Linux desktop which is far less powerful than the new Macbook Pro which is running 5.8.)
On 5.8 (updated for MacOS Catalina to the SHA above), wall clock time is 8 minutes.
The relevant code is the selftest in examples/miller/miller which is a big arithmetic normalisation.
On the Mac, memory consumption (as reported by the Activity Monitor) gets as high as 20GB; on the Linux machine running 5.7.1, the consumption remains very slight (top reports 3% in its %MEM column; the machine has 16GB)
Michael