Install HOL Light

You can install HOL Light by following its standard installation instructions.

We have included our own notes below in case they are helpful.

Install OCaml

OCaml 4.07.0 minimum is required. The easiest way to install this is through opam.

You also need to install the `num` and `camlp5` packages:

1opam install num camlp5

In many cases (including on DICE) the toplevel loads camlp4. In order to load camlp5 by default, you need to edit the .ocamlinit file in your home directory (opam usually creates one, otherwise add it yourself). Add the following to that file:

1#use "topfind";;
2#require "camlp5";;
3#load "camlp5o.cma";;

Running ocaml should give you a Camlp5 parsing version ... at the end.

Run HOL Light

To install/run HOL Light, first create the pa_j.ml file:

1make

The run ocaml and load HOL Light:

1#use "hol.ml";;

Checkpointing

Checkpointing eliminates loading times, which are otherwise relatively long, especially when you need to restart HOL Light during development.

We have been using DMTCP. Unfortunately, newer versions seem to be failing with HOL Light in a number of different platforms, but it is still worth trying.

Once you have installed DMTCP, you can create the checkpoint as follows:

1dmtcp_checkpoint ocaml

Then load HOL Light as usual:

1#use "hol.ml";;

Wait for it to finish, then open a new terminal and checkpoint:

1dmtcp_command -c

There is no notification when the checkpoint is complete other than the appearance of the dmtcp_restart_script.sh shortcut. You can then kill/exit OCaml.

Running dmtcp_restart_script.sh should load the checkpoint from where you left it. Issue a command to HOL Light/OCaml to make sure it works.

Subsequent uses of dmtcp_command -c will update your checkpoint.