Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Fetching contributors…

Cannot retrieve contributors at this time

185 lines (129 sloc) 7.225 kb
Getting and Building the HOL system
-----------------------------------
Get the HOL sources from SourceForge at http://hol.sourceforge.net
You will also need either:
the Moscow ML compiler (version 2.01) from
http://www.itu.dk/~sestoft/mosml.html
or Poly/ML, from
http://www.polyml.org
Windows users can also build the system by running a self-installing
executable (available from the above http://hol.sourceforge.net). To
do this,
1. Ensure that Moscow ML is installed first
2. Run the executable and follow the on-screen instructions.
The instructions that follow are how to build from sources, on any of
the supported operating systems
Building the HOL system
-----------------------
A. [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.
[Poly/ML:] Install the latest Poly/ML. Note that you will not be
able to use the HolBddLib example with this implementation.
http://www.polyml.org/
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
[Moscow ML:] mosml < tools/smart-configure.sml
[Poly/ML:] poly < 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
[Moscow ML:] config-override in <hol-dir>
[Poly/ML:] poly-includes.ML in <hol-dir>/tools-poly
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".
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:
[Moscow ML:] <hol-dir>/bin/build
[Poly/ML:] <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 [Moscow ML:] tools/configure.sml, [Poly/ML:]
tools-poly/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.
On Windows, the system ends up creating two copies of every object
file. To save space there, you can use the -small option, but this
has the disadvantage of forcing any subsequent builds to rebuild
everything, regardless of where changes might have occurred.
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 the hol scripts additionally include a .bat extension,
and Holmake has a .exe extension.
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 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/mn200/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.
Jump to Line
Something went wrong with that request. Please try again.