Getting and Building the Hol98 system (Working Version). --------------------------------------------------------- Get the Hol98 sources by WWW from http://www.cl.cam.ac.uk/ftp/hvg/hol98/working.tar.gz and the Moscow ML compiler (version 1.44 or greater) from http://www.dina.kvl.dk/~sestoft/mosml.html First, however, please read the rest of these instructions carefully. Building the Hol98 system. -------------------------- A. First, install Moscow ML. This is usually straightforward. The directory where it lives will be called in the following. * If you intend to use ML embeddings of C libraries, like the HolBdd library, you are so far restricted to running on Linux, Solaris, and other Unix implementations. You will have to build MoscowML from *source* in order to dynamically load C libraries, as is required by, e.g., HolBddLib. In this case, you will have to set a few shell variables; this is explained in the MoscowML installation directions. The upshot: if you are working on a Unix system, you should build MoscowML from source, making the necessary tweaks that enable dynamic linking. * If you are running on Windows, you must set the PATH and MOSMLLIB environment variables as described in the installation instructions for Moscow ML. Windows won't find the MoscowML DLL without the appropriate entry in PATH, and Moscow ML won't run without knowing where its library is. B. Unpack Hol98 with the commands gunzip working.tar.gz; tar xf working.tar in Unix, or the appropriate clicking activity in Windows NT. The resulting directory will be called in the following. When fully built, takes approximately 35M of disk space, so be sure you have enough before starting. C. Enter the "tools" directory and edit the file "configure.sml". (1) You must supply values for the following parameters: val mosmldir = val holdir = Both values must be absolute (full) pathnames. For example, my local setup has val mosmldir = "/home/kxs/mosml"; val holdir = "/home/kxs/hol98"; (2) The following parameter tells the build procedure what operating system is being used. val OS = The current choices for this are: "linux", "solaris", and "winNT". If you are on a unix operating system that is not Linux or Solaris, it is OK to just put "unix"; however, this will imply that the robdd library will not be usable (it currently only builds on linux and solaris). (3) The following parameter gives the path to a C compiler, which is used to compile the quotation preprocessor. val CC = "gcc"; This parameter may need to be changed, if "gcc" is not on your machine, or can't be found along your path. For Windows machines, we supply a prebuilt executable of the quotation preprocessoer, so if you have selected "winNT" for your OS value, then you can ignore this. Another tool that requires a C compiler to be built is the SMV tool, found in temporalLib. If a C compiler is not designated, temporalLib is still usable, but some proof procedures in it will not work. (4) The following parameter gives the path to the "gnumake" program, which is required to build the muddy library. val GNUMAKE = "gnumake"; If you are building Hol98 on an OS that is *not* Solaris or Linux, the muddy library is not currently accessible. In such a case, the value of GNUMAKE does not matter. (5) The following parameter gives the name of the local directory that Holmake uses to store its dependencies in. On Unix and WindowsNT, this name does not have to be changed. val DEPDIR = ".HOLMK"; D. Perform the following 2 shell commands: /bin/mosml < configure.sml /bin/build The first command establishes some pathnames and the like; the second actually builds the system. In case of difficulty, the configuration can be gone through by hand, by starting /bin/mosml and stepping through tools/configure.sml. Similarly, the execution of build.sml can also be stepped through in MoscowML. This can be somewhat time-consuming, but will help pinpoint any problems. E. If bin/build completes, successfully, you are done. From you can now access bin/hol * The standard Hol98 interactive system; bin/hol.unquote * The interactive system with quote preprocessing; bin/Holmake * A batch compiler for HOL directories; src/ * System sources; Manual/ * User manuals for the system; examples/ * Examples of the use of the system. External tools. ---------------- The Hol98 installation currently includes a C library (in HolBddLib) and the C sources for the SMV model-checker (in temporalLib). Both of these require a C compiler to have been specified in tools/configure.sml. Loading the BDD libraries muddyLib or HolBddLib will fail unless MoscowML has been built with dynamic linking enabled. Dealing with failure. --------------------- * If you are engaged in a large formalization, you may find a mysterious `exception 13' being raised. Please contact us if that occurs; it is a MoscowML bug and we have been supplied with a fix by Peter Sestoft. * Send a message to hol-support@cl.cam.ac.uk giving a full transcript of the failed installation. Also make sure that you include the following details: . hardware/OS the build failed on . version of MoscowML being used . version of Hol98 being built * If a build attempt fails for some reason, you should attempt to invoke bin/build -cleanAll before a new build attempt.