Thanks everyone. Now I see the issue is indeed fixed. That's great.
--Chun
On Sat, Jun 20, 2020 at 6:33 PM Phil Clayton
wrote:
> I've built HOL4 with versions of Poly/ML before and after the fix
> (c355b21 and 0ad5aa8) on Linux x86_64. I ran the miller example (with
> fixes for Poly/ML reverte
I've built HOL4 with versions of Poly/ML before and after the fix
(c355b21 and 0ad5aa8) on Linux x86_64. I ran the miller example (with
fixes for Poly/ML reverted) and it appears that 0ad5aa8 fixes the issue.
Under c355b21:
[pclayton@localhost miller]$ ./selftest.exe
Composite test on 91 ...