Getting and building the HOL system
-----------------------------------
Get the HOL sources from SourceForge at http://hol.sourceforge.net
You will also need either:
Poly/ML, from
http://www.polyml.org
or, the Moscow ML compiler (version 2.01) from
http://www.itu.dk/~sestoft/mosml.html
The instructions that follow are how to build from sources, on any of
the supported operating systems.
Building the HOL system
-----------------------
A. [Poly/ML:] Install the latest version of Poly/ML. Note that you
will not be able to use the HolBddLib example with this
implementation.
You must ensure that your dynamic library loading picks up
libpolyml.so and libpolymain.so. If these files are in /usr/lib,
you will not have to change anything, but other locations may
require further system configuration (typically done by setting the
LD_LIBRARY_PATH environment variable). A sample LD_LIBRARY_PATH
initialisation command (in a file such as ~/.bashrc) might be
declare -x LD_LIBRARY_PATH=/usr/local/lib:$HOME/lib
Do not use the --with-portable option.
[Moscow ML:] First, install Moscow ML. This is usually
straightforward. The directory where it lives will be called
<mosml-dir> in the following.
* If you intend to use ML embeddings of C libraries, like the
HolBdd library, you are so far restricted to running on Linux,
Solaris, and other Unix implementations. You will probably have
to build MoscowML from *source* in order to dynamically load C
libraries, as is required by, e.g., HolBddLib. In this case, you
will have to set a few shell variables; this is explained in the
MoscowML installation directions.
The upshot: if you are working on a Unix system, you should build
MoscowML from source, making the necessary tweaks that enable
dynamic linking. It's possible that the Moscow ML .rpm file will
work; the "binary distribution" is known not to.
* If you are running on Windows, you must set the PATH and MOSMLLIB
environment variables as described in the installation
instructions for Moscow ML. Windows won't find the MoscowML DLL
without the appropriate entry in PATH, and Moscow ML won't run
without knowing where its library is. These variables will be
set for you by the latest self-installing executable available
from the Moscow ML home-page.
B. Unpack HOL with the commands
gunzip release.tar.gz; tar xf release.tar
in Unix, or the appropriate clicking activity in Windows (use a
program like Winzip). The resulting directory will be called
<hol-dir> in the following. When fully built, <hol-dir> takes
approximately 35M of disk space, so be sure you have enough before
starting.
C. In the HOL directory (<hol-dir>), type
[Poly/ML:] poly < tools/smart-configure.sml
[Moscow ML:] mosml < tools/smart-configure.sml
This should guess some configuration options, and then build some
of HOL's support tools. If this appears to work correctly, proceed
to step D below.
If smart-configure guesses the options incorrectly, then you will
need to provide them yourself. Do this by creating a file called
[Poly/ML:] poly-includes.ML in <hol-dir>/tools-poly
[Moscow ML:] config-override in <hol-dir>
In this file provide ML bindings for as many of the values that
were incorrectly guessed by smart-configure.sml. For example, if
the holdir guess was incorrect, then put
val holdir = "a full pathname to my holdir"
for example. Most parameters must be given as ML strings, while
dynlib_available must be an ML boolean (either true or false). The
value for mosmldir must be the directory containing the Moscow ML
executables (mosml, mosmlc, etc). The value for poly must be the
path to the poly executable.
The valid values for OS are "linux", "unix", "solaris", "macosx"
and "winNT". If you are on a unix operating system that is not
Linux or Solaris, it is OK to just put "unix"; however, this will
imply that the robdd library will not be usable (it currently only
builds on linux and solaris). "winNT" stands in for all versions of
"Windows NT", "Windows 2000", "Windows XP" and "Windows Vista", and
only works for Moscow ML on Windows. If you are building with
Poly/ML on Windows, (via Cygwin or the Linux sub-system), then
don’t use "winNT" value.
It's possible that in order to get the muddy library to build, you
will need to change the binding for GNUMAKE, which is made in the
tools/configure.sml file. Edit this file if necessary to change
this binding to whatever's required:
val GNUMAKE = "gnumake";
If you are building HOL on an OS that is *not* Solaris or Linux,
the muddy library is not currently accessible. In such a case, the
value of GNUMAKE does not matter.
D. Now perform the following shell command:
<hol-dir>/bin/build
This builds the system. In case of difficulty, the configuration
can be gone through by hand, by starting the ML interpreter and
stepping through [Poly/ML:] tools-poly/configure.sml [Moscow ML:]
tools/configure.sml, by hand. Similarly, the execution of build.sml
can also be stepped through in the interpreter. This can be
somewhat time-consuming, but will help pinpoint any problems.
E. If bin/build completes (it takes a while!), successfully, you are
done. From <hol-dir> you can now access
bin/hol * The standard HOL interactive system
bin/hol.noquote * The interactive system with quote
preprocessing turned off
bin/hol.bare * A "stripped down" version of hol
bin/hol.bare.noquote * A "stripped down" version of hol.noquote,
with quote preprocessing turned off
bin/Holmake * A batch compiler for HOL directories
src/ * System sources
examples/ * Examples of the use of the system
On Windows under Moscow ML, the hol scripts additionally include a
.bat extension, and Holmake has a .exe extension.
At this point, the system is build in <hol-dir> and cannot easily
be moved to other locations. In other words, you should unpack HOL
in the location/directory where you wish to access it for all your
future work.
External tools
--------------
The HOL installation currently includes a C library (in HolBddLib),
the C sources for the SMV model-checker (in temporalLib), and for a
SAT solver (minisat) in HolSat. Building these under Unix requires a
C compiler to have been specified in tools/configure.sml. Under
Windows, precompiled binaries are available for the C library and for
minisat.
Loading the BDD libraries muddyLib or HolBddLib will fail unless
MoscowML has been built with dynamic linking enabled.
Dealing with failure
--------------------
* Send a message to hol-support@cl.cam.ac.uk giving a full transcript
of the failed installation. Please include the following details:
. hardware/OS the build failed on
. version of Moscow ML or Poly/ML being used
. version of HOL being built
* Alternatively, use the github issues web-page at
http://github.com/HOL-Theorem-Prover/HOL/issues
and submit a description of the problem.
* If a build attempt fails for some reason, you should attempt to invoke
bin/build cleanAll
from <hol-dir> before a new build attempt.