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
Description: Binary data
_______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
