hol-light-workbench /

Filename Size Date modified Message
37 B
1.1 KB
1.4 KB


This is a little script that will download, compile and install HOL Light, 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
wget https://bitbucket.org/akrauss/hol-light-workbench/raw/tip/setup
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 "hol.ml";;