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 <rda at 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 <rda at 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 at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml