Dear HOL Developers,
A problem occurred during installation of HOL4 on a MacBook Air on the basis of
the executable ML variant shipped with the current Isabelle proof assistant.
Some exceptions were raised during the build process:
"Writing HOLPage
Generating theory-graph and HTML theory signatures; this may take a while
(Use build's -nograph option to skip this step.)
---------------------------------------------------------------------
HOL-4 [Kananaskis 11 (stdknl, built Sun Aug 07 15:01:13 2016)]
For introductory HOL help, type: help "hol";
To exit type <Control>-D
---------------------------------------------------------------------
> # # # # # # # # # # # # # # # # # # # # # # # # # # # # # #
Loading system theories ..<<HOL warning: Theory.callhooks: Hook
ThmSetData.onload.compute failed on event TheoryLoaded(bft) with problem
Exception raised at clauses.enter_thm: computeLib cannot use thm
|- FINITE (Parents G) ⇒
(BFT G f seen [] acc = acc) ∧
(BFT G f seen (h::t) acc =
if MEM h seen then BFT G f seen t acc
else BFT G f (h::seen) (t ++ G h) (f h acc)):
at clauses.check_arg_form:
"f" occurs as a variable on lhs
>>
...<<HOL warning: Theory.callhooks: Hook ThmSetData.onload.compute failed on
event TheoryLoaded(dft) with problem
Exception raised at clauses.enter_thm: computeLib cannot use thm
|- FINITE (Parents G) ⇒
(DFT G f seen [] acc = acc) ∧
(DFT G f seen (visit_now::visit_later) acc =
if MEM visit_now seen then DFT G f seen visit_later acc
else
DFT G f (visit_now::seen) (G visit_now ++ visit_later)
(f visit_now acc)):
at clauses.check_arg_form:
"f" occurs as a variable on lhs
>>
...................... done
Printing HTML theories to disk ........................... done
Called dot successfully.
Hol built successfully."
In spite of these exceptions, HOL seems to run properly.
The problem can be reproduced with the following steps:
0. First, carry out a software update (OS X, Xcode, MacPorts), then install the
program 'dot' (included in the 'graphviz' package) required by HOL:
sudo port install graphviz
1. Download and install the current Isabelle software from:
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2016.dmg
2. Create an alias for the ML machine:
alias
poly='/Applications/Isabelle2016.app/Isabelle/contrib/polyml-5.6-1/x86-darwin/poly'
3. Download HOL (see: http://hol-theorem-prover.org/#get ):
git clone git://github.com/HOL-Theorem-Prover/HOL.git
4. Change directory:
cd HOL
5. Carry out some manual configuration (otherwise the build process will fail):
5a. Create file 'tools-poly/poly-includes.ML':
val polymllibdir =
"/Applications/Isabelle2016.app/Isabelle/contrib/polyml-5.6-1/x86-darwin";
val DOT_PATH = "/opt/local/bin/dot";
5b. Replace lines 2, 4, and 6 of file
'/Applications/Isabelle2016.app/Contents/Resources/Isabelle2016/contrib/polyml-5.6-1/x86-darwin/polyc':
prefix=/Users/wenzelm/lib/polyml/polyml-5.6/x86-darwin
BINDIR=${exec_prefix}/bin
LIBDIR=${exec_prefix}/lib
with
prefix=/Applications/Isabelle2016.app/Isabelle/contrib/polyml-5.6-1/x86-darwin
BINDIR=${exec_prefix}
LIBDIR=${exec_prefix}
6. Build HOL (see: http://hol-theorem-prover.org/#get ):
poly < tools/smart-configure.sml
bin/build
Kind regards,
Ken Kubota
____________________
Ken Kubota
doi: 10.4444/100
http://dx.doi.org/10.4444/100
------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
