As visible on our CI machinery at travis-ci.org, polyml?s latest git checkouts (Poly/ML 5.7 Release (Git version v5.7-283-g04d3c957)) are crashing when trying to build HOL. See for example
https://travis-ci.org/HOL-Theorem-Prover/HOL/jobs/298998364
where the end of the transcript reads
/home/travis/build/HOL-Theorem-Prover/HOL/bin/hol.state0 FAILED! <1> Loading /home/travis/build/HOL-Theorem-Prover/HOL/sigobj/boolLib error in quse /home/travis/build/HOL-Theorem-Prover/HOL/src/1/Prim_rec.sml : Fail "Exception- InternalError: codeToPRegRev raised while compiling" error in load $(HOLDIR)/src/1/Prim_rec : Fail "Exception- InternalError: codeToPRegRev raised while compiling" error in load /home/travis/build/HOL-Theorem-Prover/HOL/sigobj/boolLib : Fail "Exception- InternalError: codeToPRegRev raised while compiling" Loading /home/travis/build/HOL-Theorem-Prover/HOL/sigobj/boolLib: Fail "Exception- InternalError: codeToPRegRev raised while compiling" Exception- InternalError: codeToPRegRev raised while compiling
Michael