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
Hi David,
I'm on Mac OS X 10.11 with Xcode 8.2 (Apple LLVM 8.0) [1]. When I build latest Poly/ML sources with "--enable-compact32bit" (no others), when I execute "make compiler" (after "make"), with large chances I get the following error:
... Created functor TYPECHECK_PARSETREE Making MATCH_COMPILER Making MatchCompilerSig Created signature MatchCompilerSig Created functor MATCH_COMPILER Making CODEGEN_PARSETREE Making CodegenParsetreeSig Created signature CodegenParsetreeSig Created functor CODEGEN_PARSETREE Making PARSE_TREE Created functor PARSE_TREE Assertion failed: (space != 0), function ScanObjectAddress, file quick_gc.cpp, line 414. /bin/sh: line 1: 96770 Abort trap: 6 ./poly --error-exit < mlsource/BuildExport.sml make: *** [compiler] Error 134
The same error message (Assertion failed: (space != 0), function ScanObjectAddress, file quick_gc.cpp, line 414.) also happens multiple times (but random) when I was trying to build HOL4. Without "--enable-compact32bit" (normal 64-bit build), everything is fine.
Such an issue must be new since the last time I tested PolyML after your announcement (of "--enable-compact32bit") in the mailing list.
Hope this helps,
Chun Tian
[1] compiler information:
Apple LLVM version 8.0.0 (clang-800.0.42.1) Target: x86_64-apple-darwin15.6.0 Thread model: posix InstalledDir: /Library/Developer/CommandLineTools/usr/bin
Il 21/02/19 13:44, David Matthews ha scritto:
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
Hi, Thank you for testing this but could I ask you to re-read the second paragraph of my message. It may seem surprising but slight differences in timing can affect exactly when the garbage-collection happens and allow the compilation to work.
David
On 22/02/2019 11:51, Chun Tian (binghe) wrote:
Hi David,
I'm on Mac OS X 10.11 with Xcode 8.2 (Apple LLVM 8.0) [1]. When I build latest Poly/ML sources with "--enable-compact32bit" (no others), when I execute "make compiler" (after "make"), with large chances I get the following error:
... Created functor TYPECHECK_PARSETREE Making MATCH_COMPILER Making MatchCompilerSig Created signature MatchCompilerSig Created functor MATCH_COMPILER Making CODEGEN_PARSETREE Making CodegenParsetreeSig Created signature CodegenParsetreeSig Created functor CODEGEN_PARSETREE Making PARSE_TREE Created functor PARSE_TREE Assertion failed: (space != 0), function ScanObjectAddress, file quick_gc.cpp, line 414. /bin/sh: line 1: 96770 Abort trap: 6 ./poly --error-exit < mlsource/BuildExport.sml make: *** [compiler] Error 134
The same error message (Assertion failed: (space != 0), function ScanObjectAddress, file quick_gc.cpp, line 414.) also happens multiple times (but random) when I was trying to build HOL4. Without "--enable-compact32bit" (normal 64-bit build), everything is fine.
Such an issue must be new since the last time I tested PolyML after your announcement (of "--enable-compact32bit") in the mailing list.
Hope this helps,
Chun Tian
[1] compiler information:
Apple LLVM version 8.0.0 (clang-800.0.42.1) Target: x86_64-apple-darwin15.6.0 Thread model: posix InstalledDir: /Library/Developer/CommandLineTools/usr/bin
Il 21/02/19 13:44, David Matthews ha scritto:
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
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
Rob, Thanks for testing this and your comments. I'm replying to your individual comments below.
On 09/03/2019 16:11, Rob Arthan wrote:
- 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.)
Yes, I seem to remember that it is and that it wasn't possible to avoid it because there is a separate "configure" for libffi.
- 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.
I would always run "make distclean" before rerunning configure. Basically, what is happening is that it is picking up the wrong pre-built compiler.
- 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.
- 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.
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.
These are the assertion failure I mentioned. Did this happen after running "make compiler"?
Regards, David
David,
Thanks. I've interleaved my replies below.
On 9 Mar 2019, at 16:59, David Matthews <David.Matthews at prolingua.co.uk> wrote:
Rob, Thanks for testing this and your comments. I'm replying to your individual comments below.
On 09/03/2019 16:11, Rob Arthan wrote:
- 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.)
Yes, I seem to remember that it is and that it wasn't possible to avoid it because there is a separate "configure" for libffi.
OK. Is there a way of telling whether poly has been built with --enable-compact32bit? (So you can check whether you got what you wanted.)
- 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.
I would always run "make distclean" before rerunning configure. Basically, what is happening is that it is picking up the wrong pre-built compiler.
I'll remember to do that in future.
- 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.
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.
These are the assertion failure I mentioned. Did this happen after running "make compiler"?
My script did:
make clean make make compiler make compiler make install
and it was the "make install" that failed. I also tried it with a third "make compiler" and that didn't make any difference. Doing another "make install" failed in the same way.
Regards,
Rob.
Rob,
On 09/03/19 21:10, Rob Arthan wrote:
On 9 Mar 2019, at 16:59, David Matthews <David.Matthews at prolingua.co.uk> wrote:
- 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.
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.
These are the assertion failure I mentioned. Did this happen after running "make compiler"?
My script did:
make clean make make compiler make compiler make install
and it was the "make install" that failed. I also tried it with a third "make compiler" and that didn't make any difference. Doing another "make install" failed in the same way.
To ensure that you have two successful runs of "make compiler", it may be worth adapting the script as follows:
make clean make while ! make compiler ; do echo "** failed, retrying make compiler **" ; done while ! make compiler ; do echo "** failed, retrying make compiler **" ; done make install
Still, I can't explain why "make install" would fail - I didn't think that invoked poly if the compiler is built. I have built successfully on Fedora (25), and I'm happy to see what differs in your build if you send me your output log and config.status.
Regards, Phil
Rob, Phil and everyone else,
I'm in the process of putting together the 5.8 release and as part of that I've pushed an updated pre-built compiler for X64/32 for Linux, Mac OS etc. That means that for that platform only, for the moment, it is no longer necessary to run "make compiler", although it won't hurt. It should no longer produce the assertion fault, so if it does this is a different bug. To be absolutely sure please run "make distclean" before trying "git pull".
The pre-built compilers (in the "imports" directory) are essentially binary blobs although they are encoded as text. Since they are large and any update results in a major change to the text I try to avoid updating them more often than once for each release.
Regards, David
David,
After the "git pull", I've rebuilt Poly/ML and ProofPower and had no problems with any combination of --enable-intinf-asint, --enable-compact32bit and MacOS v. Fedora.
Poly/ML compiled with --enable-compact32bit gives me 5-8% improvement in execution times and 30-40% improvement in the size of saved states on some typical ProofPower examples. So that's a worthwhile improvement - many thanks to you and Makarius!
Regards,
Rob.
On 10 Mar 2019, at 16:30, David Matthews <David.Matthews at prolingua.co.uk> wrote:
Rob, Phil and everyone else,
I'm in the process of putting together the 5.8 release and as part of that I've pushed an updated pre-built compiler for X64/32 for Linux, Mac OS etc. That means that for that platform only, for the moment, it is no longer necessary to run "make compiler", although it won't hurt. It should no longer produce the assertion fault, so if it does this is a different bug. To be absolutely sure please run "make distclean" before trying "git pull".
The pre-built compilers (in the "imports" directory) are essentially binary blobs although they are encoded as text. Since they are large and any update results in a major change to the text I try to avoid updating them more often than once for each release.
Regards, David _______________________________________________ polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
On 10/03/2019 20:28, Rob Arthan wrote:
After the "git pull", I've rebuilt Poly/ML and ProofPower and had no problems with any combination of --enable-intinf-asint, --enable-compact32bit and MacOS v. Fedora.
Poly/ML compiled with --enable-compact32bit gives me 5-8% improvement in execution times and 30-40% improvement in the size of saved states on some typical ProofPower examples.
After some weeks with --enable-compact32bit, which Isabelle is already using by default, here is my wrap-up of it:
* The underlying architecture is x86_64, so we can discontinue the old x86 platform: it has become increasingly difficult to use that on Linux and macOS, potentially also Windows within the next few years.
* Overall stability is better than x86, which often ran into the VM boundary of less than 4GB.
* Applications that require substantial heap space run faster, sometimes much faster -- on current hardware with 8 GB RAM or more, e.g. see https://isabelle.sketis.net/devel/build_status/Mac_OS_X_10.14_High_Sierra_4_... after 21-Feb-2019.
* Old hardware with only 4GB can get into problems, with slightly degraded performance, e.g. see the particular the routine AFP measurements that are run on really ancient server machines, see https://isabelle.sketis.net/devel/build_status/AFP/index.html
Overall great work by David Matthews. We are ready for the next 10 years.
We merely need to do the final testing of big applications for the official release.
Makarius
Thanks, everyone for the testing and feedback. I've now updated the remaining prebuilt compilers and officially released 5.8 on GitHub. There is a fixes-5.8 branch but that currently just reflects master.
I'm pleased that the 32-bit under 64-bit version has proved so successful. It has involved some quite substantial changes to the storage management in the run-time system and there are still too many special cases in the code. In comparison, the differences between the 32-bit and 64-bit native address versions are quite minor.
Still, this version should be able to cope with most processors for the foreseeable future.
David
On 09/03/2019 21:10, Rob Arthan wrote:
OK. Is there a way of telling whether poly has been built with --enable-compact32bit? (So you can check whether you got what you wanted.)
PolyML.architecture();
val it = "X86_64_32": string
Word.wordSize;
val it = 31: int
LargeWord.wordSize;
val it = 64: int
David
On Thu, Feb 21, 2019 at 5:48 AM David Matthews <David.Matthews at prolingua.co.uk> wrote:
This is a last chance to test the current git master before release.
Sorry to be late. When running configure, I see this:
checking whether as supports .note.GNU-stack... yes ./configure: line 18046: dependentlibs: command not found
That is due to line 584 of configure.ac, which reads:
dependentlibs = ""
That says to invoke the dependentlibs command with two arguments: = and "". Remove the spaces around = to make it be the intended assignment.
The release looks great. I've used --enable-compact32bit with no problems. Kudos to everyone involved in making that work.
Regards,
-
binghe.lisp＠gmail.com -
David.Matthews＠prolingua.co.uk -
loganjerry＠gmail.com -
makarius＠sketis.net -
phil.clayton＠veonix.com -
rda＠lemma-one.com