Re: [Hol-info] build failed with latest HOL

2017-10-29 Thread Waqar Ahmad via hol-info
Thanks..that solves the issue...

On Mon, Oct 30, 2017 at 4:20 AM, <michael.norr...@data61.csiro.au> wrote:

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


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


Re: [Hol-info] build failed with latest HOL

2017-10-29 Thread Michael.Norrish
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.smlOK
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.state0FAILED!
 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