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.matth...@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@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
