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