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 <[email protected]> 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 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 > > <[email protected] <mailto:[email protected]>> > > > 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 < > > > [email protected] > > <mailto:[email protected]>> 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 > > >>>> > -- Chun Tian (binghe) Fondazione Bruno Kessler (Italy)
_______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
