Installing HOL4 (Kananaskis 10) from Sources

The HOL4 source distribution is available as a gzipped tar file from a SourceForge mirror.

The instructions that follow explain in detail how to download and then install HOL 4 on your machine.

Installing an SML Implementation

HOL4 is implemented in SML, which means that you need an SML implementation (compiler and interactive loop) to run it. In fact, HOL4 currently requires either Poly/ML or Moscow ML. If you are working on Windows, you must use Moscow ML, but otherwise we highly recommend using Poly/ML, which is much faster.

(If you already have a ML installation, you can skip this step.)


To use Poly/ML with HOL, you must be on a non-Windows system. You will need to download the appropriate tar-file from the Poly/ML download page, and then install from sources, as per the instructions there. Note also that Poly/ML 5.5.1 does not work unless installed with the --enable-shared flag. This option must be passed to the invocation of configure that is the first step of building Poly/ML from sources.

HOL4 requires at least Poly/ML 5.2.

Moscow ML

With an existing Moscow ML implementation (at least in version 2.01), you may find that your installation is crashing unexpectedly with strange Chr exceptions. If so, you will probably want to follow the instructions on rebuilding Moscow ML to avoid this.)

On Unix:

Download and install one of the appropriate distribution files from either the old or new Moscow ML home-pages. As of early November 2014, there are source distributions for versions 2.01 and 2.10.1; both are fine.

Check that you can run mosml. In what follows, we’ll assume that you have installed in /mosml, so that the interpreter is at /mosml/bin/mosml. Wherever you see /mosml in what follows, please substitute whatever you have actually chosen.

Note that the instructions for building from source in "install-linux.txt" suggest running a test in /mosml/src/test. This test doesn’t work, so don’t worry if you try it and it fails!

Make sure that you follow instructions about enabling dynamic linking.

On Windows:


Download the Windows binary distribution and follow these instructions. In particular, check that you can run mosml. If you can’t it’ll probably be because you haven’t set your environment variables (PATH and MOSMLLIB) correctly.


Use the automatic self-extracting archive, and run this. If you don't have adminstrator privileges on the machine where you run this, you will need to set the environment variables (as above) manually.


Use the installer for version 2.10.1.

The text to come assumes that you have built in a directory called /mosml. This doesn’t make total sense in the Windows environment, but please substitute whatever you have chosen to be mosml’s home (c:\program files\mosml say) for /mosml whenever you see the latter.

On Mac OS X

When editing mosml/src/, in the section for compiling with dynamically loadable libraries, comment out the existing sections and add the following lines for Mac OS X:


Later in the file mosml/src/, in the section for compiler and linker options, comment out the existing option sets and create the following new option set:

   # For Mac OS X 10.x.y (Intel or PowerPC), use:
   # --------------------------------------------
   CPP=/usr/bin/cpp -no-cpp-precomp -P -traditional -Dunix -Umsdos
   DYNLD=gcc -bundle -bundle_loader ${MOSMLHOME}/bin/camlrunm

Then run:

   make world
   make install

To use the Moscow ML dynamic libraries, before you run make world, etc. make sure that you set the environment variable DYLD_LIBRARY_PATH to include the directory MOSMLHOME/lib (as described in the installation instructions of Moscow ML).

As an example of how to set the appropriate environment variables, here is the relevant portion of a sample .bashrc file:

   # Libraries

   # Add Moscow ML 2.01 to the path

   export MOSMLHOME

Moscow ML is distributed with a number of dynamic libraries. HOL4 doesn’t need any of these itself, but you may wish to add them to your Moscow ML implementation. If so, and if you’re on a Unix-like system, you’ll have to build each of the dynamic libraries that you need yourself, by the following general procedure:

  1. cd MOSMLHOME/src/dynlibs/DYNLIB
  2. make all
  3. cp libDYNLIB ../../../lib/

There are minor problems with two dynamic libraries on Mac OS X. In the munix library the file munix.c contains a switch statement for errno that includes a case ELIBBAD entry. This error code does not exist on Mac OS X, so comment out this case. In the crypt library the Makefile contains a reference to -lcrypt, and this needs to be changed to -lcrypto.

Some of the dynamic libraries implement the make install command in their Makefiles, which can then be used in place of the cp command above.

Installing HOL

To download HOL, use the link at the top or bottom of this page. When you unpack this tarball, it will create a directory called hol-kananaskis-10. Change to that directory and execute

   MLSYS < tools/smart-configure.sml

where MLSYS is either mosml or poly. If doing this on Windows, you will need to write tools\smart-configure.sml

This should guess an approriate configuration for your setup. If it fails to do so, please see Chapter 1 of the Tutorial for a way of overriding smart-configure’s guesses.

Finally, build hol by executing


(again, reverse the slash if on Windows.)

After much output, the bin/hol executable, and many useful theories will have been built.

Download HOL sources

Anonymous Git Access

It is also possible to use git to download (and regularly update) the current version of the development repository on github.

See these instructions on how to access the repository anonymously.

Time-stamp: "Tuesday, 18 November 2014; 22:37 UTC (Michael Norrish)"