This is a little script that will download, compile and install HOL
, including
compatible versions of OCaml and Camlp5. This is a very quick and
easy way to get things up and running, even if the distribution does
not provide suitable packages for OCaml.

All installation is local to a given directory (say, under your home
directory). No root permissions are required.

This script was tested on Linux (both 32 and 64 bit). It might also
work on other Unix-like systems, possibly with modifications.


Download the script. (Alternatively, you can also clone this repository.)

mkdir hol-light-workbench
cd hol-light-workbench
chmod 755 setup

Run the script.


The installer creates a little script with shell environment settings (PATH
etc.). Import it into the current shell as follows to adjust the paths.

. setpaths

Now, you can run HOL Light as follows:

cd hol-light
# #use "";;