Hi Anthony,
I checked my installation of HOL, minisat was successfully compiled and the
blastlib test did not use the internal prover.
I downloaded a clean version of HOL from github and recompiled it, and
after that, my compilation of examples/machine-code was not getting stuck
anymore. However, I encountered the compile error below:
/Users/jiaqi/code/HOL.latest/bin/Holmake: Finished recursive invocation in
/Users/jiaqi/code/HOL.latest/examples/machine-code/instruction-set-models/x86_64
Analysing codegenLib.sig
Trying to create directory .HOLMK for dependency files
Analysing codegenLib.sml
Analysing codegen_armLib.sig
Analysing codegen_inputLib.sig
Analysing codegen_ppcLib.sig
Analysing codegen_x64Lib.sig
Analysing codegen_x86Lib.sig
Analysing codegen_armLib.sml
Analysing codegen_inputLib.sml
Analysing codegen_ppcLib.sml
Analysing codegen_x64Lib.sml
Analysing codegen_x86Lib.sml
Analysing compilerLib.sig
Analysing compilerLib.sml
Analysing reg_allocLib.sig
Analysing reg_allocLib.sml
/Users/jiaqi/code/HOL.latest/bin/Holmake: Finished recursive invocation in
/Users/jiaqi/code/HOL.latest/examples/machine-code/compiler
/Users/jiaqi/code/HOL.latest/bin/Holmake: Recursively calling Holmake in
/Users/jiaqi/code/HOL.latest/examples/machine-code/compiler/demo
Analysing compiler_demoScript.sml
Trying to create directory .HOLMK for dependency files
/Users/jiaqi/code/HOL.latest/bin/buildheap -o local-hol-heap ../compilerLib
Poly/ML 5.5.1 Release
val heapname = "local-hol-heap": string
Loading ../compilerLib
ld: warning: could not create compact unwind for _ffi_call_unix64: does not
use RBP or RSP based frame
Linking compiler_demoScript.uo to produce theory-builder executable
Poly/ML 5.5.1 Release
Error- in 'poly/poly-init2.ML', line 156.
Type error in function application.
Function: Word.fromLargeWord : Word.largeword -> word
Argument: (PolyWord8.toLargeWord w) : word
Reason:
Can't unify Word.largeword (*Created from opaque signature*) with
word (*In Basis*) (Different type constructors)
Found near Word.fromLargeWord (PolyWord8.toLargeWord w)
Exception- Fail "Static Errors" raised
Cannot find file compiler_demoScript.ui
Cannot find file compiler_demoScript.ui
/Users/jiaqi/code/HOL.latest/bin/Holmake: Failed script build for
compiler_demoScript - exited with code 1
/Users/jiaqi/code/HOL.latest/bin/Holmake: Finished recursive invocation in
/Users/jiaqi/code/HOL.latest/examples/machine-code/compiler/demo
Build failed in directory examples/machine-code/ (exited with code 1)
However, I do have compiler_demoScript.sml in
examples/machine-code/compiler/demo.
Thanks,
Jiaqi
On Sat, Apr 5, 2014 at 5:29 AM, Anthony Fox <ac...@cam.ac.uk> wrote:
> I think it’s more likely that there was a problem with building minisat
> under the latest Mac OS. To check that it is installed, try going to the
> directory
>
> HOL/src/HolSat/sat_solvers/minisat
>
> There should be a binary “minisat” there. Alternatively, to make sure it
> is working properly, you can try something like:
>
> > load “blastLib”;
> ..
> > blastLib.BBLAST_PROVE ``?x y. x + y = 12w : word8``;
>
> If you see the warning
>
> HolSat WARNING: SAT solver not found. Using slow internal prover.
> To turn off this warning, type: set_trace "HolSatLib_warn" 0; RET
>
> then that is the source of your problem.
>
> I have a patch for the minisat sources, but it’s not been checked on other
> platforms yet.
>
> Anthony
>
> On 5 Apr 2014, at 08:09, Ramana Kumar <ram...@member.fsf.org> wrote:
>
> > I believe it takes several hours. I haven't done it myself though.
> >
> >
> > On Sat, Apr 5, 2014 at 3:23 AM, Jiaqi Tan <tanji...@cmu.edu> wrote:
> > Hi,
> >
> > I have downloaded the latest version of HOL from github, and my current
> build of examples/machine-code is taking quite a long time, and the build
> has been stuck in examples/machine-code/instruction-set-models/x86_64 for
> about an hour. I'm wondering if that's normal.
> >
> > I am using PolyML 5.5.1 on Mac OS X 10.9.2. I have built HOL (poly <
> tools/smart-configure.sml followed by bin/build), and I am building
> examples/machine-code using "bin/build -dir examples/machine-code".
> >
> > The last couple of lines of console output are:
> >
> > Exporting theory "prog_x64" ... done.
> > Theory "prog_x64" took 13.609s to build
> > Analysing prog_x64Theory.sig
> > Analysing prog_x64Theory.sml
> > Linking prog_x64_extraScript.uo to produce theory-builder executable
> > Poly/ML 5.5.1 Release
> > <<HOL message: Created theory "prog_x64_extra">>
> > Saved definition __ "zCODE_HEAP_RAX_def"
> > [cache]Saved definition __ "IMM32_def"
> > Saved definition __ "stack_list_def"
> > Saved definition __ "stack_list_rev_def"
> > Saved definition __ "stack_ok_def"
> > Saved definition __ "zSTACK_def"
> > Saved theorem _____ "x64_pop_r0"
> > Saved theorem _____ "x64_pop_r1"
> > Saved theorem _____ "x64_pop_r2"
> > Saved theorem _____ "x64_pop_r3"
> > Saved theorem _____ "x64_pop_r6"
> > Saved theorem _____ "x64_pop_r7"
> > Saved theorem _____ "x64_pop_r8"
> > Saved theorem _____ "x64_pop_r9"
> > Saved theorem _____ "x64_pop_r10"
> > Saved theorem _____ "x64_pop_r11"
> > Saved theorem _____ "x64_pop_r12"
> > Saved theorem _____ "x64_pop_r13"
> > Saved theorem _____ "x64_pop_r14"
> > Saved theorem _____ "x64_pop_r15"
> >
> > How long does it typically take to build examples/machine-code? Is it
> closer to under an hour, or several hours?
> >
> > Thanks!
> >
> > Regards,
> > Jiaqi
> >
> >
> >
> ------------------------------------------------------------------------------
> >
> > _______________________________________________
> > hol-info mailing list
> > hol-info@lists.sourceforge.net
> > https://lists.sourceforge.net/lists/listinfo/hol-info
> >
> >
> >
> ------------------------------------------------------------------------------
> > _______________________________________________
> > hol-info mailing list
> > hol-info@lists.sourceforge.net
> > https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
