That’s a Poly/ML bug. Please use the 5.7 release available at
https://github.com/polyml/polyml/archive/v5.7.tar.gz
Michael
From: Waqar Ahmad via hol-info <hol-info@lists.sourceforge.net>
Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Saturday, 28 October 2017 at 18:13
To: hol-info <hol-info@lists.sourceforge.net>
Subject: [Hol-info] build failed with latest HOL
Hi all,
I'm installing the latest HOL (Github version) in Ubuntu. The installation of
the polyml v5.7.1 went successfully. However, the building of HOL failed with
following error message:
waqar@waqar-VirtualBox:~/Downloads/HOL/HOL$ bin/build
*** Using kernel option -stdknl from earlier build command;
use -expk, -otknl, or -stdknl to override
*** Using -j 2 from earlier build command; use -j to override
Cleaning out /home/waqar/Downloads/HOL/HOL/sigobj
/home/waqar/Downloads/HOL/HOL/sigobj cleaned
*** Build log exists; new logging will concatenate onto this file
Building directory tools/mlyacc/mlyacclib [28 اكتوبر, 11:36:46]
Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj
Building directory src/portableML/poly [28 اكتوبر, 11:36:49]
Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj
Building directory src/portableML [28 اكتوبر, 11:37:03]
FunctionalRecordUpdate.sml OK
GetOpt.sig OK
GetOpt.sml OK
Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj
Building directory src/portableML/monads [28 اكتوبر, 11:37:32]
Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj
Building directory src/prekernel [28 اكتوبر, 11:37:41]
Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj
Building directory src/0 [28 اكتوبر, 11:38:01]
Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj
Building directory src/postkernel [28 اكتوبر, 11:38:11]
Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj
Building directory src/parse [28 اكتوبر, 11:38:21]
base_lexer.sml OK
Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj
Building directory src/opentheory [28 اكتوبر, 11:39:29]
Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj
Building directory src/bool [28 اكتوبر, 11:39:33]
boolTheory OK
Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj
Building directory src/1 [28 اكتوبر, 11:39:49]
DiskFiles.lex.sml OK
DiskFiles.grm-sig.sml DiskFiles.grm.sml OK
DiskFiles.grm-sig.sml DiskFiles.grm.sml OK
ConseqConvTheory OK
Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj
Building directory src/proofman [28 اكتوبر, 11:41:00]
/home/waqar/Downloads/HOL/HOL/bin/hol.state0 FAILED!
error in quse /home/waqar/Downloads/HOL/HOL/src/1/Prim_rec.sml : Fail
"Exception- InternalError: codeToPRegRev raised while compiling"
error in load /home/waqar/Downloads/HOL/HOL/src/1/Prim_rec : Fail "Exception-
InternalError: codeToPRegRev raised while compiling"
error in load boolLib : Fail "Exception- InternalError: codeToPRegRev raised
while compiling"
Exception- InternalError: codeToPRegRev raised while compiling
Build failed in directory /home/waqar/Downloads/HOL/HOL/src/proofman (exited
with code 1)
I wonder whether this error is due to polyml or HOL.. Can anybody help me in
fixing this issue?
--
Waqar Ahmed, Ph.D.
System Analysis and Verification (SAVe) Lab
School of Electrical Engineering and Computer Science (SEECS)
National University of Science and Technology (NUST), H-12, Islamabad, Pakistan
Web: http://save.seecs.nust.edu.pk/waqar-ahmad/
[http://research.bournemouth.ac.uk/wp-content/uploads/2014/02/NUST_Logo2.png]
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info