Many thanks for this speedy fix!
Michael
On 20/6/20, 03:23, "polyml on behalf of David Matthews"
wrote:
Hi,
You did run "make compiler" at least once after running "configure" and
"make", didn't you?
David
On 19/06/2020 18:17, Chun Tian (binghe) wrote:
> Hi David,
>
> I rebuilt and install
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 ...
Hi David,
no I didn't do "make compiler" in my previous tests... But after I did it
(make compiler; make install) and rebuilt HOL, the "miller" selftest result
is the same. The whole testing process still need more than 8 minutes to
finish.
Regards,
Chun
On Sat, Jun 20, 2020 at 1:23 AM David
Hi,
You did run "make compiler" at least once after running "configure" and
"make", didn't you?
David
On 19/06/2020 18:17, Chun Tian (binghe) wrote:
Hi David,
I rebuilt and installed PolyML 5.8 ('master', up to 0ad5aa8) and ran again
the 'miller' selftests as Michael mentioned, but the result
Hi David,
I rebuilt and installed PolyML 5.8 ('master', up to 0ad5aa8) and ran again
the 'miller' selftests as Michael mentioned, but the results seem unchanged:
```
Composite test on 91 ...
(0.018s) OK
Composite test on 123 ... [GC = 0.037]
(0.013s)
Thanks, Phil, for reminding me of this. I've committed a fix (0ad5aa8)
for that. There was a tail-recursive function in your example that
returned a tuple. Poly/ML puts these on the stack where it can but in
this case it was causing the function to cease to be tail-recursive,
eating up the s
I also found that 5.8 can consume a huge amount of memory compared to
5.7.1. In my case, it was a very small example doing simple arithmetic
operations (demonstrating Fermat's method to find pairs of factors) so
it may be related. I have raised an issue for it:
https://github.com/polyml/polym
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
