David, Apologies! This was all down to a simple misunderstanding on my part. I hadn't appreciated that --enable-compact32bit gives you 31-bit ints. My proof search explores in excess of 2^32 blind alleys and it tries to count them.
The confusion about Mac OS versions and lldb was caused by me doing the tests with the compiler built with --enable-intinf-as-int as well as --enable-compact32bit. Regards, Rob. > On 3 Apr 2019, at 18:41, Rob Arthan <r...@lemma-one.com> wrote: > > David, > > >> On 2 Apr 2019, at 11:34, David Matthews <david.matth...@prolingua.co.uk> >> wrote: >> >> Rob, >> Have you tried using the Poly debugger? >> PolyML.Compiler.debug := true; >> open PolyML.Debug; >> breakEx Overflow; >> then compile your code. >> >> This won't help if the problem is a code-generator bug because adding the >> debugging code may well change the code and avoid the bug but if it's a >> library function this may narrow it down. >> > It ran to completion after about 6 hours. So compiling for debugging does > avoid the bug. Is there anything > I can do with gdb? I’ll have a think about instrumenting my code with > exception handlers to try to pinpoint > the problem. > > Regards, > > Rob. > >> Regards, >> David >> >> On 31/03/2019 13:31, Rob Arthan wrote: >>> I have done some further experiments. I can reproduce the problem on >>> Mac OS Mojave 10.14.4 >>> Fedora 24 >>> Kubuntu 18.10 >>> The above were all run an iMac using VirtualBox VMs for the Linux >>> distros. >>> I also tried running poly under a debugger and found that the problem >>> doesn’t occur when run under lldb on Mac OS Mojave. It does occur >>> when run under gdb on the two Linux distros. >>> Regards, >>> Rob >>>> On 31 Mar 2019, at 00:04, Rob Arthan <r...@lemma-one.com> wrote: >>>> >>>> The tarball did survive the mailing list and I've just unpacked it and >>>> tried >>>> the test on my MacBook. The problem does not occur on a MacBook >>>> running Mac OS High Sierra 10.13.6 but does occur on an iMac >>>> running Mac OS Mojave 10.14.4. >>>> >>>> I'll try it on some Linux VMs tomorrow. >>>> >>>> Regards, >>>> >>>> Rob. >>>> >>>>> On 30 Mar 2019, at 16:50, Rob Arthan <r...@lemma-one.com> wrote: >>>>> >>>>> I was doing some performance comparisons and found what looks like a bug >>>>> in Poly/ML >>>>> when compiled with —enable-compact32bit. The problem is that ML code that >>>>> runs to completion when compiled to use native 64 bit addresses, raises >>>>> Overflow >>>>> when compiled to 32 bit addressing. The code is a lengthy proof search >>>>> that explores in excess of 4,000,000,000 blind alleys. It takes about >>>>> 10 to 20 minutes to find the proof when using 64 bit addressing >>>>> and it takes 2 or 3 minutes before it raises Overflow when using 32 bit >>>>> addressing. >>>>> >>>>> I don’t really know where to start with narrowing the problem down. I’ve >>>>> attached a tarball >>>>> containing cutdown source that demonstrates the problem, but the mailing >>>>> list >>>>> software will likely strip it off, hence CC to David. >>>>> >>>>> Regards, >>>>> >>>>> Rob. >>>>> <fordavidm20190330.tgz>_______________________________________________ >>>>> 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 >>> _______________________________________________ >>> 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 _______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
