David,
I?ve been trying building and testing ProofPower on the various combinations of MacOS Mojave v. Linux Fedora 24, ?enable-compact32bit v. ?disable-compact32bit and ?enable-intinf-asint and ?disable-intinf-asint and have a few observations.
1) The configure script doesn?t validate an option beginning "?enable-?. So I didn?t notice that I?d mistyped ?enable-compact32bit until I realised that I was getting executables and saved states with almost identical sizes. (I appreciate that this may be an autoconfig thing that you can?t control.)
2) If you build Poly/ML with ?disable-compact32bit and then try to build it with ?enable-compact32 without doing ?make clean", it will fail during the ?make install? step like this:
Making install in . ./polyimport polytemp.txt -I . < ./exportPoly.sml Assertion failed: (j >= -(((POLYSIGNED)0x80 << (POLYSIGNED)(8*(sizeof(PolyWord)-1) -1)) -1)-1 && j <= (((POLYSIGNED)0x80 << (POLYSIGNED)(8*(sizeof(PolyWord)-1) -1)) -1)), function GetValue, file pexport.cpp, line 461. /bin/sh: line 1: 46725 Abort trap: 6 ./polyimport polytemp.txt -I . < ./exportPoly.sml make[1]: *** [polyexport.o] Error 134 make: *** [install-recursive] Error 1
Doing ?make clean? solves this problem.
3) On MacOS with ?disable-intinf-asint and ?enable-compact32bit, the ProofPower build fails like this:
Assertion failed: (space != 0), function ScanObjectAddress, file quick_gc.cpp, line 414.
4) On Fedora with ?enable-intinf-asint and ?enable-compact32bit, the ProofPower build fails like this:
pp-ml: quick_gc.cpp:414: virtual PolyObject* QuickGCScanner::ScanObjectAddress(PolyObject*): Assertion `space != 0' failed.
I can attempt to give you cut-down code to reproduce (3) and (4) if the above error messages don?t give you enough of a clue.
Regards,
Rob.
On 21 Feb 2019, at 12:44, David Matthews <David.Matthews at prolingua.co.uk> wrote:
The current version of Poly/ML is approaching the point of creating a new release, 5.8. Makarius has run a lot of tests with Isabelle and various bugs have been fixed. This has mainly affected the 32-bit object ID version for 64-bits but some of the fixes will also have affected the native-address versions.
This is a last chance to test the current git master before release. Don't forget to run "make compiler" at least twice after the initial "make" in order to build the up-to-date compiler and recompile all the code with it. This is particularly important if testing the --enable-compact32bit version. Some extra checking was added during testing and there is a strong chance of getting an assertion failure during the initial "make" or the first "make compiler" due to a bug in the pre-built compiler. If this happens just rerun the step. Once the compiler has been rebuilt it will incorporate a fix.
David
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml