hol90 Installation Guide

To build hol90 takes four stages:
  1. Get the hol90 sources
  2. Get SML/NJ
  3. Make hol90
  4. Install the hol90 manual
If it happens that you want to move the system after it has been built, consult Moving hol90 after it has been built. If you have any trouble building the system, please send mail to
Important! Once you have installed the system, all users must rebuild any theories (and libraries that build theories) that have been built on an earlier release of hol90.

User Manual Table of Contents

Get the hol90 sources

These are available by anonymous ftp from either Munich or Bell Labs

Once you have the hol90 source, it it can be unpacked by

    zcat hol90.7.tar.Z | tar xf -
This gives a directory called hol90, with the following directories:

Beginning of Installation Guide.
User Manual Table of Contents.


Currently, hol90 is being implemented in the SML/NJ dialect of SML. It has some dependencies on that compiler, although ports to PolyML and other compilers have been successfully carried out in the past. For now, though, the New Jersey compiler is what you need. The New Jersey compiler has a well-deserved reputation for being memory hungry. You can run hol90 on a 16 Megabyte Sun workstation, but the more memory the better! A workstation with 24 Megabytes or more, with generous swap space is recommended. The current public release of the SML/NJ compiler is available from Bell Labs.

Beginning of Installation Guide.
User Manual Table of Contents.

Make hol90

For this release, we assume that theory files will be represented in ascii on disk. Currently this is preferable because ascii theories are architecture independent and orders of magnitude smaller than binary theories. If you have an intense desire to build binary theory files, send mail to the author of this document. The model for building the hol90 system is simply to make the system image for every architecture of interest. In the following sml is a copy of the SML/NJ compiler (with perhaps some other functions added, e.g., the SML/NJ library). The notation .../hol90 represents the full path to the hol90 sources.

In the simplest case, making the system image for an architecture is done by invoking the unix command

    make_hol sml
in the directory .../hol90/src. This will leave an image hol90.arch, where arch is what SML/NJ thinks is the machine architecture. It takes about 20 minutes on a SPARC10, and considerably longer for some other machines.

There are extra options to make_hol that cover special circumstances, so if you find that the default option to make_hol doesn't give you the flexibility you need to build hol90 at your site, the following documentation gives more detail.


The calling convention for make_hol is:
    make_hol sml [-n | -b | -o] [-d path]
The default, calling make_hol sml with no parameters, tells the system to The other options are
Reuse the existing ascii theory files.

This option tells the system to rebuild all its theories. Be warned that a consequence of this option is that the system libraries will have to be rebuilt (with src/make_lib) and all user theories at the site will have to be rebuilt, along with any images that depend on hol90 libraries.

The -b option tells the system to build binary theories. This is not advised, and some editing of the src/sys01.sml file is necessary to get this approach to work.

-d path
This option to make_hol is used to establish the root directory for hol90. If your current directory at the time of calling make_hol is not .../hol90/src, then you will need to supply the full directory path to the hol90 directory. This option is also useful in the case when building a version of the system that will be used in a networked environment, where the root directory may be expanded differently for different machines in the network. Note: there must be a space separating -d and path.
The default invocation for building the system is equivalent to invoking
    make_hol sml -o -d `pwd`/..
in .../hol90/src.



Please note that in this release the system libraries do not have to be built; that has already been done for you. However, if one rebuilds the system with the -n option, then libraries must be rebuilt. This is done with src/make_lib; the invocation is
    make_lib hol90


In this release the contributed libraries do have to be built after hol90 has been made (if you want to use a contrib library). This is done with src/make_contrib; the invocation is
    make_contrib hol90
Notes. Beginning of Installation Guide.
User Manual Table of Contents.

Install the hol90 manual

The hol90 manual is hyperlinked, and is mostly self-contained. However, it does provide links to the local SML/NJ installation, in the file doc/sml.html. The paths in this file should be adjusted to the paths for your local setup.

Beginning of Installation Guide.
User Manual Table of Contents.

Moving hol90 after it has been built

One may decide to move hol90 after it has been built. There are a couple of scenarios that have been considered by the hol90 implementors:

Finally, once this new version of hol90 has been installed, we repeat that all hol90 users must rebuild any of their theories that have been built on an earlier release of hol90.

Beginning of Installation Guide.
User Manual Table of Contents.
Konrad Slind, slind@informatik.tu-muenchen.de