Getting and Building the HOL system ----------------------------------- Get the HOL sources by WWW from http://www.cl.cam.ac.uk/Research/HVG/FTP/ or from SourceForge (links to which are on the page above). You will also need the Moscow ML compiler (version 2.00) from http://www.dina.kvl.dk/~sestoft/mosml.html First, however, please read the rest of these instructions carefully. Windows users can also build the system by running a self-installing executable (available from the above places). To do this, 1. Ensure that Moscow ML is installed first 2. Run the executable and follow the on-screen instructions. The instructions that follow are how to build from sources, on any of the supported operating systems Building the HOL 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 probably 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. It's possible that the Moscow ML .rpm file will work; the "binary distribution" is known not to. * 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 HOL with the commands gunzip release.tar.gz; tar xf release.tar in Unix, or the appropriate clicking activity in Windows NT (use a program like Winzip). 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 type mosml < smart-configure.sml ------------------------------ This should guess some configuration options, and then build some of HOL's support tools. If this appears to work correctly, proceed to step D below. If smart-configure guesses the options incorrectly, then you will need to provide them yourself. Do this by creating a file called config-override in . In this file provide ML bindings for as many of the values that were incorrectly guessed by smart-configure.sml. For example, if the holdir guess was incorrect, then put val holdir = "a full pathname to my holdir" for example. All three parameters must be given as ML strings. The valid values for OS are "linux", "unix", "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). "winNT" stands in for all versions of "Windows NT", "Windows 2000", and (we believe) "Windows XP". It's possible that in order to get the muddy library to build, you will need to change the binding for GNUMAKE, which is made in the tools/configure.sml file. Edit this file if necessary to change this binding to whatever's required: val GNUMAKE = "gnumake"; If you are building HOL 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. D. Now perform the following shell command: /bin/build This 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. The build program ends up creating two copies of every ML object file. To save space on Unix, use the -symlink option. This option is not available on Windows, unfortunately. To save space there, you can use the -small option, but this has the disadvantage of forcing any subsequent builds to rebuild everything, regardless of where changes might have occurred. E. If bin/build completes, successfully, you are done. From you can now access bin/hol * The standard HOL interactive system; bin/hol.unquote * The interactive system with quote preprocessing; bin/hol.bare * A "stripped down" version of hol bin/hol.bare.unquote * A "stripped down" version of hol.unquote 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 HOL 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. --------------------- * 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 HOL being built * Alternatively, use the Support tracker web-page at http://sourceforge.net/tracker/?func=add&group_id=31790&atid=403398 and submit a request for support. You can also use the Bugs forum on SourceForge. * If a build attempt fails for some reason, you should attempt to invoke bin/build -cleanAll before a new build attempt.