Re: [polyml] Horrific GC(?) behaviour in 5.8 (g44efa473)

2020-06-20 Thread Chun Tian (binghe)
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

Re: [polyml] Horrific GC(?) behaviour in 5.8 (g44efa473)

2020-06-20 Thread Phil Clayton
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 ...