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.
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.
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.)
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.
Either:
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 (PATHandMOSMLLIB) correctly.
Or:
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.
Or:
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.
When editing mosml/src/Makefile.inc, in the section for
compiling with dynamically loadable libraries, comment out the existing
sections and add the following lines for Mac OS X:
ADDPRIMS=dynlib.c
ADDOBJS=dynlib.o
ADDRUNLIBS=-L${MOSMLHOME}/lib -ldl
ADDRUNCFLAGS=-I${MOSMLHOME}/include
ADDDYNLIBCFLAGS=
Later in the file mosml/src/Makefile.inc, 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
STRIP=echo
LD=gcc
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
DYLD_LIBRARY_PATH=/usr/lib:/usr/local/lib
# Add Moscow ML 2.01 to the path
MOSMLHOME=${HOME}/mosml
DYLD_LIBRARY_PATH=${DYLD_LIBRARY_PATH}:${MOSMLHOME}/lib
PATH=${PATH}:${MOSMLHOME}/bin
export DYLD_LIBRARY_PATH 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:
cd MOSMLHOME/src/dynlibs/DYNLIBmake all
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.
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
bin/build
(again, reverse the slash if on Windows.)
After much output, the bin/hol executable, and many useful theories will have been built.
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.