Re: [Hol-info] advice on installing Ocaml, camlp5 & HOL Light on Mac OS X 10.8.5?

[Marco M. <mar...@gm...>]

2014-09-17 14:14 GMT+02:00 Nela Cicmil <nel...@dp...>:

> and all seemed to complete without errors. My question is, if HOL Light is
> now installed on my machine, what's the best way to run it?


​Sorry, I forgot to say.  As you already found yourself, you have to use
the command

hol_light

which starts ocaml and loads hol.ml automatically.

You have to wait a few minutes while the full system loads (people use
checkpointing precisely to avoid this step).  Don't care about the long
list of messages and warnings, all should be OK.  At the end you get
something like:

File
"/nix/store/0cgxqn0x9nz0i6l5ysnf9ak0rqkh0v7y-hol_light-189/lib/hol_light/
help.ml", line 116, characters 25-57:

Warning 3: deprecated feature: operator (&); you should use (&&) instead

Camlp5 parsing version 6.11


#

then you can type our commands: e.g.

# ARITH_RULE `1 + 1 = 2`;;
val it : thm =

|- 1 + 1 = 2


Small suggestion: since the ocaml toplevel do not have line editing
features, you may want to use rlwrap:


nix-env -i rlwrap


then invoke hol as


rlwrap hol_light


Hope it helps and keep asking if all this is not clear,

Marco