Hi Anthony, Thank you for the pointer, Holmake worked for me, I was indeed using "build" to try to build the examples. I have managed to compile examples/machine-code.
Regards, Jiaqi On Sat, Apr 5, 2014 at 3:15 PM, Anthony Fox <ac...@cam.ac.uk> wrote: > Hi Jiaqi, > > I get the same error if I do > > bin/build -dir examples/machine-code > > so I suspect this is problem with “build”. The more conventional thing to > do would be: > > $ cd HOL/examples/machine-code > $ Holmake > > This should enable you to get a bit further. The machine-code example is > pretty demanding — it helps to have a machine with lots of RAM. > > Thanks, > Anthony > > On 5 Apr 2014, at 19:31, Jiaqi Tan <jia...@andrew.cmu.edu> wrote: > > > 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
