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.