2014-09-17 14:14 GMT+02:00 Nela Cicmil <nela.cic...@dpag.ox.ac.uk>:
> 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
------------------------------------------------------------------------------
Want excitement?
Manually upgrade your production database.
When you want reliability, choose Perforce
Perforce version control. Predictably reliable.
http://pubads.g.doubleclick.net/gampad/clk?id=157508191&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
