Dear Ken,
Thank you for the error report. The warning messages are ugly, and not
helpful. As you supposed, the system's behaviour won't have been affected, but
it's still not a good look. The bug has now been fixed on the master branch
(commits 8f675fb and f44f111 by Anthony Fox).
Best wishes,
Michael
On 8/08/2016, 21:31, "Ken Kubota" <m...@kenkubota.de> wrote:
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
------------------------------------------------------------------------------
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are
consuming the most bandwidth. Provides multi-vendor support for NetFlow,
J-Flow, sFlow and other flows. Make informed decisions using capacity
planning reports. http://sdm.link/zohodev2dev
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
