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/
------------------------------------------------------------------------------
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
