Getting and Installing HOL

This chapter describes how to get the HOL system and how to install it. It is generally assumed that some sort of Unix system is being used, but the instructions that follow should apply mutatis mutandis to other platforms. Unix is not a pre-requisite for using the system. HOL may be run on PCs running Windows operating systems from Windows NT onwards (i.e., Windows 2000, XP and Vista are also supported), as well as Macintoshes running MacOS X.

Getting HOL

The HOL system can be downloaded from http://hol-theorem-prover.org. The naming scheme for HOL releases is $\langle$name$\rangle$-$\langle$number$\rangle$; the release described here is \holnversion.

The hol-info mailing list

The hol-info mailing list serves as a forum for discussing HOL and disseminating news about it. If you wish to be on this list (which is recommended for all users of HOL), visit http://lists.sourceforge.net/lists/listinfo/hol-info. This web-page can also be used to unsubscribe from the mailing list.

Installing HOL

It is assumed that the HOL sources have been obtained and the tar file unpacked into a directory hol.¹ The contents of this directory are likely to change over time, but it should contain the following:

The session in the box below shows a typical distribution directory. The HOL distribution has been placed on a PC running Linux in the directory /home/mn200/hol/.

All sessions in this documentation will be displayed in boxes with a number in the top right hand corner. This number indicates whether the session is a new one (when the number will be 1) or the continuation of a session started in an earlier box. Consecutively numbered boxes are assumed to be part of a single continuous session. The Unix prompt for the sessions is $, so lines beginning with this prompt were typed by the user. After entering the HOL system (see below), the user is prompted with - for an expression or command of the HOL meta-language SML; lines beginning with this are thus SML expressions or declarations. Lines not beginning with $ or - are system output. Occasionally, system output will be replaced with a line containing ... when it is of minimal interest. The meta-language SML is introduced in Chapter 2.

$ pwd
/home/mn200/hol
$ ls -F
CONTRIBUTORS    README          doc/            sigobj/         tools/
COPYRIGHT       bin/            examples/       src/            tools-poly/
INSTALL         developers/     help/           std.prelude

Now you will need to rebuild HOL from the sources.²

Before beginning you must have a current version of Poly/ML or Moscow ML.³ In the case of Moscow ML, you must have at least version 2.01. Poly/ML is available from http://polyml.org. Moscow ML is available on the web from http://mosml.org.

When working with Poly/ML, the installation must ensure that dynamic library loading (typically done by setting the LD_LIBRARY_PATH environment variable) picks up libpolyml.so and libpolymain.so. If these files are in /usr/lib, nothing will need to be changed, but other locations may require further system configuration. 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.

When you have your ML system installed, and are in the root directory of the distribution, the next step is to run smart-configure. With Moscow ML, this looks like:

$ mosml < tools/smart-configure.sml
Moscow ML version 2.01 (January 2004)
Enter `quit();' to quit.
- [opening file "tools/smart-configure-mosml.sml"]

HOL smart configuration.

Determining configuration parameters: OS mosmldir holdir
OS:                 linux
mosmldir:           /home/mn200/mosml/bin
holdir:             /home/mn200/hol
dynlib_available:   true

Configuration will begin with above values.  If they are wrong
press Control-C.

If you are using Poly/ML, then write

   poly < tools/smart-configure.sml

instead.

Assuming you don't interrupt the configuration process, this will build the Holmake and build programs, and move them into the hol/bin directory. If something goes wrong at this stage, consult Section 1.3.1 below.

The next step is to run the build program. This should result in a great deal of output as all of the system code is compiled and the theories built. Eventually, a HOL system⁴ is produced in the bin/ directory.

$ bin/build
  ...
  ...
Uploading files to /home/mn200/hol/sigobj

Hol built successfully.
$

At this point, the system is build in your HOL directory, 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.

Overriding smart-configure

If smart-configure is unable to guess correct values for the various parameters (holdir, OS etc.) then you can create a file called to provide correct values. With Poly/ML, this should be poly-includes.ML in the tools-poly directory. With Moscow ML, this should be config-override in the root directory of the HOL distribution. In this file, specify the correct value for the appropriate parameter by providing an ML binding for it. All variables except dynlib_available must be given a string as a possible value, while dynlib_available must be either true or false. So, one might write

val OS = "unix";
val holdir = "/local/scratch/myholdir";
val dynlib_available = false;

The config-override file need only provide values for those variables that need overriding.

With this file in place, the smart-configure program will use the values specified there rather than those it attempts to calculate itself. The value given for the OS variable must be one of "unix", "linux", "solaris", "macosx" or "winNT".⁵

In extreme circumstances it is possible to edit the file tools/configure.sml yourself to set configuration variables directly. (If you are using Poly/ML, you must edit tools-poly/configure.sml instead.) At the top of this file various incomplete SML declarations are present, but commented out. You will need to uncomment this section (remove the (* and *) markers), and provide sensible values. All strings must be enclosed in double quotes.

The holdir value must be the name of the top-level directory listed in the first session above. The OS value should be one of the strings specified in the accompanying comment.

When working with Poly/ML, the poly string must be the path to the poly executable that begins an interactive SML session. The polymllibdir must be a path to a directory that contains the file libpolymain.a. When working with Moscow ML, the mosmldir value must be the name of the directory containing the Moscow ML binaries (mosmlc, mosml, mosmllex etc).

Subsequent values (CC and GNUMAKE) are needed for “optional” components of the system. The first gives a string suitable for invoking the system's C compiler, and the second specifies a make program.

After editing, tools/configure.sml the lines above will look something like:

$ more configure.sml
  ...
val mosmldir = "/home/mn200/mosml";
val holdir   = "/home/mn200/hol";
val OS       = "linux"       (* Operating system; choices are:
                                "linux", "solaris", "unix", "winNT" *)

val CC       = "gcc";     (* C compiler (for building quote filter)        *)
val GNUMAKE  = "gnumake"; (* for robdd library                             *)
  ...
$

Now, at either this level (in the tools or tools-poly directory) or at the level above, the script configure.sml must be piped into the SML interpreter (i.e., mosml or poly). For example,

$ mosml < tools/configure.sml
Moscow ML version 2.01 (January 2004)
Enter `quit();' to quit.
- > val mosmldir = "/home/mn200/mosml" : string
  val holdir = "/home/mn200/hol" : string
  val OS = "linux" : string
- > val CC = "gcc" : string
  ...
Beginning configuration.
- Making bin/Holmake.
  ...
Making bin/build.
- Making hol98-mode.el (for Emacs)
- Setting up the standard prelude.
- Setting up src/0/Globals.sml.
- Generating bin/hol.
- Attempting to compile quote filter ... successful.
- Setting up the muddy library Makefile.
- Setting up the help Makefile.
-
Finished configuration!
-
$

1. You may choose another name if you want; it is not important. ↩

2. It is possible that pre-built systems may soon be available from the web-page mentioned above. ↩

3. We recommend using Poly/ML on all operating systems, but it requires Cygwin or the Windows Linux sub-system on Windows. ↩

4. The hol executable supports --bare for a minimal environment. With Moscow ML, --noquote disables the quotation filter; with Poly/ML, --poly starts with no HOL state. ↩

5. The string "winNT" is used for Microsoft Windows operating systems that are at least as recent as Windows NT. This includes Windows 2000, XP, Vista, Windows 10 etc. Do not use "winNT" when using Poly/ML via Cygwin or the Linux sub-system. ↩