Installing Moscow ML 2.01 and HOL 4 (Kananaskis 4) from Sources

The HOL 4 source distribution is available as a gzipped tar file from a SourceForge mirror.

The instructions that follow explain in detail how to download and then install Moscow ML and HOL 4 on your machine.

Installing Moscow ML

(If you already have a Moscow ML installation, you can skip this step.)

On Unix:

Download and install one of the appropriate distribution files from the Moscow ML home-page. (Anything except the “Linux (libc 6) executables with documentation” should be fine.) As of early March 2004, there is only a source distribution of Moscow ML 2.01 available, but this may change.

Check that you can run mosml. In what follows, we’ll assume that you have installed in /mosml, so that the interpreter is at /mosml/bin/mosml. Wherever you see /mosml in what follows, please substitute whatever you have actually chosen.

Note that the instructions for building from source in "install-linux.txt" suggest running a test in /mosml/src/test. This test doesn’t work, so don’t worry if you try it and it fails!

Make sure that you follow instructions about enabling dynamic linking.

On Windows:

Either:

Download the Windows binary distribution and follow these instructions. In particular, check that you can run mosml. If you can’t it’ll probably be because you haven’t set your environment variables (PATH and MOSMLLIB) correctly.

Or:

Use the automatic self-extracting archive, and run this. If you don't have adminstrator privileges on the machine where you run this, you will need to set the environment variables (as above) manually.

The text to come assumes that you have built in a directory called /mosml. This doesn’t make total sense in the Windows environment, but please substitute whatever you have chosen to be mosml’s home (c:\program files\mosml say) for /mosml whenever you see the latter.

On Mac OS X

When editing mosml/src/Makefile.inc, in the section for compiling with dynamically loadable libraries, comment out the existing sections and add the following lines for Mac OS X:

   ADDPRIMS=dynlib.c 
   ADDOBJS=dynlib.o 
   ADDRUNLIBS=-L${MOSMLHOME}/lib -ldl 
   ADDRUNCFLAGS=-I${MOSMLHOME}/include 
   ADDDYNLIBCFLAGS= 

Later in the file mosml/src/Makefile.inc, in the section for compiler and linker options, comment out the existing option sets and create the following new option set:

   # For Mac OS X 10.x.y (Intel or PowerPC), use:
   # --------------------------------------------
   CPP=/usr/bin/cpp -no-cpp-precomp -P -traditional -Dunix -Umsdos
   STRIP=echo
   LD=gcc
   DYNLD=gcc -bundle -bundle_loader ${MOSMLHOME}/bin/camlrunm

Then run:

   make world 
   make install 

To use the Moscow ML dynamic libraries, before you run make world, etc. make sure that you set the environment variable DYLD_LIBRARY_PATH to include the directory MOSMLHOME/lib (as described in the installation instructions of Moscow ML).

As an example of how to set the appropriate environment variables, here is the relevant portion of a sample .bashrc file:

   # Libraries
   DYLD_LIBRARY_PATH=/usr/lib:/usr/local/lib

   # Add Moscow ML 2.01 to the path
   MOSMLHOME=${HOME}/mosml
   DYLD_LIBRARY_PATH=${DYLD_LIBRARY_PATH}:${MOSMLHOME}/lib
   PATH=${PATH}:${MOSMLHOME}/bin

   export DYLD_LIBRARY_PATH PATH
   export MOSMLHOME

You’ll have to build each of the dynamic libraries that you need yourself, by the following general procedure:

1. cd MOSMLHOME/src/dynlibs/DYNLIB
2. make all
3. cp libDYNLIB ../../../lib/

There are minor problems with two dynamic libraries on Mac OS X. In the munix library the file munix.c contains a switch statement for errno that includes a case ELIBBAD entry. This error code does not exist on Mac OS X, so comment out this case. In the crypt library the Makefile contains a reference to -lcrypt, and this needs to be changed to -lcrypto.

Some of the dynamic libraries implement the make install command in their Makefiles, which can then be used in place of the cp command above.

Installing HOL

To download HOL, use the link at the top or bottom of this page. When you unpack this tarball, it will create a directory called hol. We ll assume this is /hol in what comes below.

In the /hol directory, execute

   /mosml/bin/mosml < /hol/tools/smart-configure.sml

This should guess an approriate configuration for your setup. If it fails to do so, please see Chapter 1 of the Tutorial for a way of overriding smart-configure’s guesses.

Finally, build hol by executing

   /hol/bin/build 

(again, reverse those slashes if on Windows.)

On Unix systems, add the option -symlink for a slightly faster build and a system that is easier to update.

After much output, the /hol/bin/hol executable, and many useful theories will have been built.

Download HOL sources

Anonymous CVS Access

It is also possible to use CVS to download (and regularly update) the current version of the development repository on SourceForge.

See these instructions on how to access the repository anonymously.