MODERN HOL LIGHT
Modern HOL Light is an experimental rewrite of the HOL Light interactive
theorem prover / proof checker. It is based on the same source (kinda, sorta).
The current main goal is to get rid of its custom syntax and make it use
standard OCaml syntax, though I have more thoughts about where I want to take it.
OBS!!! This repo just contains parts of the HOL Light core and is not very usable
in itself.
This is the root of the Github code repository:
https://github.com/joharasmus/modern-hol-light
Basic installation instructions are below. The installation currently
recommends OCaml 4.14.0.
* * * * * * * *
INSTALLATION
The Objective CAML (OCaml) implementation is a prerequisite for
running HOL Light. You will also need camlp5.
1. OCaml + opam: there are packages for many Linux distributions. For
example, on a debian derivative like Ubuntu, you just need
to do the following:
sudo apt install ocaml opam
Once installed, run
opam init
to set up the default opam "switch". You can have multiple switches
in opam, one for each version of OCaml. Set up one for OCaml
4.14.0, by
opam switch create 4.14.0
and start using it with
opam switch set 4.14.0
2. HOL Light dependency packages: The Modern HOL Light system requires the
package num:
opam install num
3. Frontend (optional): The builtin OCaml front-end is very simple, I prefer to use
"utop" which one gets with
opam install utop
4. Editor (optionaler): I prefer to use VSCode, which you can download at
https://code.visualstudio.com
If you choose to use VSCode, install the "OCaml Platform" plugin
for better OCaml integration. The plugin requires another opam package:
opam install ocaml-lsp-server
* * * * * * * * * *
Now for HOL Light itself. The instructions below assume a Unix-like
environment such as Linux [or WSL (Windows Subsystem for Linux) under
Windows], but the steps automated by the Makefile are easy enough to
invoke manually. There's more detail on doing that in the Tutorial.
(0) You can download the HOL Light sources from the Github site.
For example, the following will copy the code from the trunk of the
Github repository into a new directory 'modern-hol-light':
git clone https://github.com/joharasmus/modern-hol-light
The above is the recommended way of getting HOL Light. You should next
enter the 'modern-hol-light' directory that has been created:
cd ./modern-hol-light
(1) Run 'utop'. You should see a prompt. At the prompt '#' you need to enter
'#use "hol.ml";;' (the '#' is part of the command, not the prompt)
in order to load HOL Light. This should rebuild all the core HOL Light
theories, which will output all the core theories to the terminal, and
terminate after a few minutes, something like:
val search : term list -> (string * thm) list = <fun>
- : unit = ()
File "help.ml" already loaded
- : unit = ()
- : unit = ()
- : unit = ()
#
HOL Light is now ready for the user to start proving theorems. You
can also use the load process in other directories, but
you should either set the environment variable HOLLIGHT_DIR to point
to the directory containing the HOL source files, or change the
first line of "hol.ml" to give that explicitly, from
let hol_dir = ref (try Sys.getenv "HOLLIGHT_DIR" with Not_found -> Sys.getcwd());;
to, for example
let hol_dir = "/home/johnh/modern-hol-light";;
or
let hol_dir = "/usr/share/modern-hol-light";;