How to install Moscow ML 2.01 and HOL-4 under Linux
===================================================

This file explains how to install HOL-4 (previously HOL98) in the directory
/home/mjcg/HOL4 on my Linux machine at Cambridge. To create
instructions for your Linux machine edit this file by replacing
"/home/mjcg/HOL4" with the absolute path name of the
directory in which you want to install hol.

First create the directory 

 /home/mjcg/HOL4
 
Download "source files with documentation" for Moscow ML
("Version 2.01 for Unixes") from

 http://www.dina.dk/~sestoft/mosml.html

N.B. It is safest to to rebuild Moscow ML from sources,
     though the Linux RedHat RPM binaries might work. 

The Moscow ML sources can either be downloaded via the web page, or by

 cd /home/mjcg/HOL4

and then by executing

 wget http://www.dina.kvl.dk/~sestoft/mosml/mos201src.tar.gz

To build Moscow ML, first unpack the distribution by executing

 tar xvzf mos201src.tar.gz
 
Next edit

 /home/mjcg/HOL4/mosml/src/Makefile.inc

so that MOSMLHOME is defined as:

 MOSMLHOME=/home/mjcg/HOL4/mosml

Then

 cd /home/mjcg/HOL4/mosml/src/

and execute 

 make world
 make install

This should build Moscow ML.  Note that the instructions
"install-linux.txt" suggest running a test in
/home/mjcg/HOL4/mosml/src/test.  This test doesn't work, so
don't worry if you try it and it fails!

For installing HOL98 under Linux nothing else needs to be done.  In
particular, the HOL98 installation will take care of dynamic linking,
so (B4*) in "install-linux.txt" can be ignored.

To download hol98

 cd /home/mjcg/HOL4

and then download the hol98 sources into it from SourceForge. If you are not
a developer (see http://www.cl.cam.ac.uk/~mjcg/SourceForge.html) then

 cvs -d:pserver:anonymous@cvs.sourceforge.net:/cvsroot/hol login

   (press the Enter key (return) when asked for a password)

 cvs -z3 -d:pserver:anonymous@cvs.sourceforge.net:/cvsroot/hol co hol98

If you are a developer, then

 export CVS_RSH=ssh 
 cvs -z3 -d:ext:mjcg@cvs.sourceforge.net:/cvsroot/hol co hol98

The next step is to build hol98. Edit

  /home/mjcg/HOL4/hol98/tools/configure.sml

so that mosmldir and holdir are set to the appropriate strings:

 val mosmldir = "/home/mjcg/HOL4/mosml";
 val holdir   = "/home/mjcg/HOL4/hol98";

Note that you may need to un-comment the definitions of mosmldir and
holdir.  Next ensure OS is correctly set

 val OS       = "linux";

Next

 cd /home/mjcg/HOL4/hol98/tools 

and then execute

 /home/mjcg/HOL4/mosml/bin/mosml < configure.sml

Finally, build hol by executing

 /home/mjcg/HOL4/hol98/bin/build -symlink 

The "-symlink" is needed so that updates to libraries, specifically
HolBddLib, see below, can easily be made. 

N.B. If a rebuild is being done, then in occasional pathological cases
     you might need to precede the build by

        /home/mjcg/HOL4/hol98/bin/build cleanAll 

     The message saying sigobj/CVS can't be removed can be safely ignored.

After much output (see build-log) the following executable
should have been built:

 /home/mjcg/HOL4/hol98/bin/hol.unquote


---------------------------------------------------------------------
Mike Gordon
Wed Sep 19 12:23:51 BST 2001
Wed Aug  9 13:24:57 BST 2006