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 ...
(0.024s) OK
Composite test on 123 ...
(0.016s) OK
Composite test on 4294967297 ...
[GC = 3.401] (0.394s) OK
Composite test on 18446744073709551617 ...
[GC = 186.871] (3.216s) OK
Composite test on 340282366920938463463374607431768211457 ...
^C^C
Under 0ad5aa8:
[pclayton@localhost miller]$ ./selftest.exe
Composite test on 91 ...
[GC = 0.027] (0.023s) OK
Composite test on 123 ...
(0.018s) OK
Composite test on 4294967297 ...
(0.360s) OK
Composite test on 18446744073709551617 ...
(2.540s) OK
Composite test on 340282366920938463463374607431768211457 ...
(19.700s) OK
Chun - your Poly/ML build commands (make compiler; make install) don't
specify "make compiler" after "make" - see
https://www.polyml.org/download.html
I wonder therefore whether the compiler was rebuilt in your test.
Phil
On 20/06/20 04:32, Chun Tian (binghe) wrote:
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 Matthews
<david.matth...@prolingua.co.uk <mailto:david.matth...@prolingua.co.uk>>
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 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) OK
> Composite test on 4294967297 ... [GC
= 3.487]
> (0.376s) OK
> Composite test on 18446744073709551617 ... [GC
= 84.370]
> (2.846s) OK
> Composite test on 340282366920938463463374607431768211457 ... [GC =
> 429.267] (21.935s) OK
>
> real 9m19.723s
> user 9m7.408s
> sys 0m12.139s
> ```
>
> I'm on macOS 10.15 (catalina) with 2,3 GHz Intel Core i9 (8
core). The same
> tests took less than 30s with PolyML 5.7.
>
> Hope this helps,
>
> Chun Tian
>
>
> On Fri, Jun 19, 2020 at 6:54 PM David Matthews <
> david.matth...@prolingua.co.uk
<mailto:david.matth...@prolingua.co.uk>> wrote:
>
>> 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 stack. The reason for the regression was a change
in the
>> way tuples on the stack are handled in the 32-in-64 bit
version. Your
>> example now works as it used to.
>>
>> Michael, it would be worth trying your code with the latest
version to
>> see if this has fixed it. If it hasn't then presumably it's a
different
>> problem and I'll have to investigate further.
>>
>> David
>>
>> On 16/06/2020 09:58, Phil Clayton wrote:
>>> 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/polyml/issues/121
>>>
>>> Phil
>>>
>>> On 16/06/20 02:30, Norrish, Michael (Data61, Acton) wrote:
>>>> 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
>>>>
>>>>
>>>>
>>>> _______________________________________________
>>>> polyml mailing list
>>>> polyml@inf.ed.ac.uk <mailto:polyml@inf.ed.ac.uk>
>>>> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
>>>>
>>> _______________________________________________
>>> polyml mailing list
>>> polyml@inf.ed.ac.uk <mailto:polyml@inf.ed.ac.uk>
>>> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
>> _______________________________________________
>> polyml mailing list
>> polyml@inf.ed.ac.uk <mailto:polyml@inf.ed.ac.uk>
>> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
>
>
>
>
> _______________________________________________
> polyml mailing list
> polyml@inf.ed.ac.uk <mailto:polyml@inf.ed.ac.uk>
> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
>
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk <mailto:polyml@inf.ed.ac.uk>
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
--
Chun Tian (binghe)
Fondazione Bruno Kessler (Italy)
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
