1Getting and building the HOL system 2----------------------------------- 3 4Get the HOL sources from SourceForge at http://hol.sourceforge.net 5 6You will also need either: 7 8Poly/ML, from 9 10 http://www.polyml.org 11 12or, the Moscow ML compiler (version 2.01) from 13 14 http://www.itu.dk/~sestoft/mosml.html 15 16The instructions that follow are how to build from sources, on any of 17the supported operating systems. 18 19 20Building the HOL system 21----------------------- 22 23A. [Poly/ML:] Install the latest version of Poly/ML. Note that you 24 will not be able to use the HolBddLib example with this 25 implementation. 26 27 You must ensure that your dynamic library loading picks up 28 libpolyml.so and libpolymain.so. If these files are in /usr/lib, 29 you will not have to change anything, but other locations may 30 require further system configuration (typically done by setting the 31 LD_LIBRARY_PATH environment variable). A sample LD_LIBRARY_PATH 32 initialisation command (in a file such as ~/.bashrc) might be 33 34 declare -x LD_LIBRARY_PATH=/usr/local/lib:$HOME/lib 35 36 Do not use the --with-portable option. 37 38 [Moscow ML:] First, install Moscow ML. This is usually 39 straightforward. The directory where it lives will be called 40 <mosml-dir> in the following. 41 42 * If you intend to use ML embeddings of C libraries, like the 43 HolBdd library, you are so far restricted to running on Linux, 44 Solaris, and other Unix implementations. You will probably have 45 to build MoscowML from *source* in order to dynamically load C 46 libraries, as is required by, e.g., HolBddLib. In this case, you 47 will have to set a few shell variables; this is explained in the 48 MoscowML installation directions. 49 50 The upshot: if you are working on a Unix system, you should build 51 MoscowML from source, making the necessary tweaks that enable 52 dynamic linking. It's possible that the Moscow ML .rpm file will 53 work; the "binary distribution" is known not to. 54 55 * If you are running on Windows, you must set the PATH and MOSMLLIB 56 environment variables as described in the installation 57 instructions for Moscow ML. Windows won't find the MoscowML DLL 58 without the appropriate entry in PATH, and Moscow ML won't run 59 without knowing where its library is. These variables will be 60 set for you by the latest self-installing executable available 61 from the Moscow ML home-page. 62 63B. Unpack HOL with the commands 64 65 gunzip release.tar.gz; tar xf release.tar 66 67 in Unix, or the appropriate clicking activity in Windows (use a 68 program like Winzip). The resulting directory will be called 69 <hol-dir> in the following. When fully built, <hol-dir> takes 70 approximately 35M of disk space, so be sure you have enough before 71 starting. 72 73C. In the HOL directory (<hol-dir>), type 74 75 [Poly/ML:] poly < tools/smart-configure.sml 76 [Moscow ML:] mosml < tools/smart-configure.sml 77 78 This should guess some configuration options, and then build some 79 of HOL's support tools. If this appears to work correctly, proceed 80 to step D below. 81 82 If smart-configure guesses the options incorrectly, then you will 83 need to provide them yourself. Do this by creating a file called 84 85 [Poly/ML:] poly-includes.ML in <hol-dir>/tools-poly 86 [Moscow ML:] config-override in <hol-dir> 87 88 In this file provide ML bindings for as many of the values that 89 were incorrectly guessed by smart-configure.sml. For example, if 90 the holdir guess was incorrect, then put 91 92 val holdir = "a full pathname to my holdir" 93 94 for example. Most parameters must be given as ML strings, while 95 dynlib_available must be an ML boolean (either true or false). The 96 value for mosmldir must be the directory containing the Moscow ML 97 executables (mosml, mosmlc, etc). The value for poly must be the 98 path to the poly executable. 99 100 The valid values for OS are "linux", "unix", "solaris", "macosx" 101 and "winNT". If you are on a unix operating system that is not 102 Linux or Solaris, it is OK to just put "unix"; however, this will 103 imply that the robdd library will not be usable (it currently only 104 builds on linux and solaris). "winNT" stands in for all versions of 105 "Windows NT", "Windows 2000", "Windows XP" and "Windows Vista", and 106 only works for Moscow ML on Windows. If you are building with 107 Poly/ML on Windows, (via Cygwin or the Linux sub-system), then 108 don���t use "winNT" value. 109 110 It's possible that in order to get the muddy library to build, you 111 will need to change the binding for GNUMAKE, which is made in the 112 tools/configure.sml file. Edit this file if necessary to change 113 this binding to whatever's required: 114 115 val GNUMAKE = "gnumake"; 116 117 If you are building HOL on an OS that is *not* Solaris or Linux, 118 the muddy library is not currently accessible. In such a case, the 119 value of GNUMAKE does not matter. 120 121D. Now perform the following shell command: 122 123 <hol-dir>/bin/build 124 125 This builds the system. In case of difficulty, the configuration 126 can be gone through by hand, by starting the ML interpreter and 127 stepping through [Poly/ML:] tools-poly/configure.sml [Moscow ML:] 128 tools/configure.sml, by hand. Similarly, the execution of build.sml 129 can also be stepped through in the interpreter. This can be 130 somewhat time-consuming, but will help pinpoint any problems. 131 132E. If bin/build completes (it takes a while!), successfully, you are 133 done. From <hol-dir> you can now access 134 135 bin/hol * The standard HOL interactive system 136 bin/hol.noquote * The interactive system with quote 137 preprocessing turned off 138 bin/hol.bare * A "stripped down" version of hol 139 bin/hol.bare.noquote * A "stripped down" version of hol.noquote, 140 with quote preprocessing turned off 141 bin/Holmake * A batch compiler for HOL directories 142 src/ * System sources 143 examples/ * Examples of the use of the system 144 145 On Windows under Moscow ML, the hol scripts additionally include a 146 .bat extension, and Holmake has a .exe extension. 147 148 At this point, the system is build in <hol-dir> and cannot easily 149 be moved to other locations. In other words, you should unpack HOL 150 in the location/directory where you wish to access it for all your 151 future work. 152 153 154External tools 155-------------- 156 157The HOL installation currently includes a C library (in HolBddLib), 158the C sources for the SMV model-checker (in temporalLib), and for a 159SAT solver (minisat) in HolSat. Building these under Unix requires a 160C compiler to have been specified in tools/configure.sml. Under 161Windows, precompiled binaries are available for the C library and for 162minisat. 163 164Loading the BDD libraries muddyLib or HolBddLib will fail unless 165MoscowML has been built with dynamic linking enabled. 166 167 168Dealing with failure 169-------------------- 170 171* Send a message to hol-support@cl.cam.ac.uk giving a full transcript 172 of the failed installation. Please include the following details: 173 174 . hardware/OS the build failed on 175 . version of Moscow ML or Poly/ML being used 176 . version of HOL being built 177 178* Alternatively, use the github issues web-page at 179 180 http://github.com/HOL-Theorem-Prover/HOL/issues 181 182 and submit a description of the problem. 183 184* If a build attempt fails for some reason, you should attempt to invoke 185 186 bin/build cleanAll 187 188 from <hol-dir> before a new build attempt. 189