1\chapter{Getting and Installing \HOL{}} 2\label{install} 3 4This chapter describes how to get the \HOL{} system and how to install 5it. It is generally assumed that some sort of Unix system is being 6used, but the instructions that follow should apply {\it mutatis 7 mutandis\/} to other platforms. Unix is not a pre-requisite for 8using the system. \HOL{} may be run on PCs running Windows operating 9systems from Windows~NT onwards (i.e., Windows~2000, XP and Vista are 10also supported), as well as Macintoshes running MacOS~X. 11 12\section{Getting \HOL{}} 13 14The \HOL{} system can be downloaded from \url{http://hol-theorem-prover.org}. 15The naming scheme for \holn{} releases is $\langle${\it name}$\rangle$-$\langle${\it number}$\rangle$; the release described here is \holnversion. 16 17\section{The {\tt hol-info} mailing list} 18 19The \texttt{hol-info} mailing list serves as a forum for discussing 20\HOL{} and disseminating news about it. If you wish to be on this 21list (which is recommended for all users of \HOL), visit 22\url{http://lists.sourceforge.net/lists/listinfo/hol-info}. This 23web-page can also be used to unsubscribe from the mailing list. 24 25\section{Installing \HOL{}} 26 27It is assumed that the \HOL{} sources have been obtained and the 28\texttt{tar} file unpacked into a directory \ml{hol}.\footnote{You may 29 choose another name if you want; it is not important.} The contents 30of this directory are likely to change over time, but it should 31contain the following: 32 33\begin{center} 34\begin{tabular}{|l|l|l|} \hline 35\multicolumn{3}{|c|}{ } \\ 36\multicolumn{3}{|c|}{\bf Principal Files on the HOL Distribution Directory} \\ 37\multicolumn{3}{|c|}{ } \\ 38{\it File name} & {\it Description} & {\it File type} \\ \hline 39{\tt README} & Description of directory {\tt hol} & Text\\ 40{\tt COPYRIGHT}& A copyright notice & Text\\ 41{\tt INSTALL} & Installation instructions & Text\\ 42{\tt tools} & Source code for building the system & Directory\\ 43{\tt bin} & Directory for HOL executables & Directory\\ 44{\tt sigobj} & Directory for \ML{} object files & Directory\\ 45{\tt src} & \ML{} sources of \HOL & Directory\\ 46{\tt help} & Help files for \HOL{} system & Directory\\ 47{\tt examples} & Example source files & Directory\\ 48\hline 49\end{tabular} 50\end{center} 51 52The session in the box below shows a typical distribution directory. 53The \HOL{} distribution has been placed on a PC running Linux in the 54directory {\small\tt /home/mn200/hol/}. 55 56All sessions in this documentation will be displayed in boxes with a 57number in the top right hand corner. This number indicates whether 58the session is a new one (when the number will be {\small\sl 1}) or 59the continuation of a session started in an earlier box. 60Consecutively numbered boxes are assumed to be part of a single 61continuous session. The Unix prompt for the sessions is 62\texttt{\small \dol}, so lines beginning with this prompt were typed 63by the user. After entering the \HOL{} system (see below), the user 64is prompted with {\small\verb|-|} for an expression or command of the 65\HOL{} meta-language \ML; lines beginning with this are thus \ML\ 66expressions or declarations. Lines not beginning with \texttt{\small 67 \$} or {\small\verb|-|} are system output. Occasionally, system 68output will be replaced with a line containing {\small\verb|...|} when 69it is of minimal interest. The meta-language \ML{} is introduced in 70Chapter~\ref{ML}. 71 72\setcounter{sessioncount}{0} 73\begin{session} 74\begin{verbatim} 75$ pwd 76/home/mn200/hol 77$ ls -F 78CONTRIBUTORS README doc/ sigobj/ tools/ 79COPYRIGHT bin/ examples/ src/ tools-poly/ 80INSTALL developers/ help/ std.prelude 81\end{verbatim} 82\end{session} 83 84Now you will need to rebuild \HOL{} from the sources.\footnote{It is 85 possible that pre-built systems may soon be available from the 86 web-page mentioned above.} 87 88Before beginning you must have a current version of Poly/ML or Moscow~ML.\footnote{We recommend using Poly/ML on all operating systems, but it requires Cygwin or the Windows Linux sub-system on Windows.} 89In the case of Moscow~ML, you must have at least version 2.01. 90Poly/ML is available from \url{http://polyml.org}. 91Moscow~ML is available on the web from \url{http://mosml.org}. 92 93When working with Poly/ML, the installation must ensure that dynamic library loading (typically done by setting the \texttt{LD\_LIBRARY\_PATH} environment variable) picks up \texttt{libpolyml.so} and \texttt{libpolymain.so}. 94If these files are in \texttt{/usr/lib}, nothing will need to be changed, but other locations may require further system configuration. 95A sample \texttt{LD\_LIBRARY\_PATH} initialisation command (in a file such as \texttt{.bashrc}) might be 96\begin{verbatim} 97 declare -x LD_LIBRARY_PATH=/usr/local/lib:$HOME/lib 98\end{verbatim} 99Do not use the \texttt{--with-portable} option. 100 101When you have your ML system installed, and are in the root directory of the distribution, the next step is to run \texttt{smart-configure}. 102With Moscow~ML, this looks like: 103 104\begin{session} 105\begin{alltt} 106\dol mosml < tools/smart-configure.sml 107Moscow ML version 2.01 (January 2004) 108Enter `quit();' to quit. 109- [opening file "tools/smart-configure-mosml.sml"] 110 111HOL smart configuration. 112 113Determining configuration parameters: OS mosmldir holdir 114OS: linux 115mosmldir: /home/mn200/mosml/bin 116holdir: /home/mn200/hol 117dynlib_available: true 118 119Configuration will begin with above values. If they are wrong 120press Control-C. 121\end{alltt} 122\end{session} 123 124If you are using Poly/ML, then write 125\begin{verbatim} 126 poly < tools/smart-configure.sml 127\end{verbatim} 128instead. 129 130Assuming you don't interrupt the configuration process, this will 131build the \texttt{Holmake} and \texttt{build} programs, and move them 132into the \texttt{hol/bin} directory. If something goes wrong at this 133stage, consult Section~\ref{sec:editting-configure} below. 134 135The next step is to run the \texttt{build} program. This should 136result in a great deal of output as all of the system code is compiled 137and the theories built. Eventually, a \HOL{} system\footnote{Four 138 \HOL{} executables are produced: \textsf{hol}, \textsf{hol.noquote}, 139 \textsf{hol.bare} and \textsf{hol.bare.noquote}. The first of these 140 will be used for most examples in the \TUTORIAL{}.} is produced in 141the \texttt{bin/} directory. 142 143\begin{session} 144\begin{alltt} 145\dol bin/build 146 ... 147 ... 148Uploading files to /home/mn200/hol/sigobj 149 150Hol built successfully. 151\dol 152\end{alltt} 153\end{session} 154 155At this point, the system is build in your HOL directory, and cannot easily be moved to other locations. 156In other words, you should unpack HOL in the location/directory where you wish to access it for all your future work. 157 158 159 160\subsection{Overriding \texttt{smart-configure}} 161\label{sec:editting-configure} 162 163If \texttt{smart-configure} is unable to guess correct values for the various parameters (\texttt{holdir}, \texttt{OS} \etc) then you can create a file called to provide correct values. 164With Poly/ML, this should be \texttt{poly-includes.ML} in the \texttt{tools-poly} directory. 165With Moscow~ML, this should be \texttt{config-override} in the root directory of the HOL distribution. 166In this file, specify the correct value for the appropriate parameter by providing an ML binding for it. 167All variables except \texttt{dynlib\_available} must be given a string as a possible value, while \texttt{dynlib\_available} must be either \texttt{true} or \texttt{false}. 168So, one might write 169 170\begin{session} 171\begin{verbatim} 172val OS = "unix"; 173val holdir = "/local/scratch/myholdir"; 174val dynlib_available = false; 175\end{verbatim} 176\end{session} 177 178The \texttt{config-override} file need only provide values for those 179variables that need overriding. 180 181With this file in place, the \texttt{smart-configure} program will use 182the values specified there rather than those it attempts to calculate 183itself. The value given for the \texttt{OS} variable must be one of 184\texttt{"unix"}, \texttt{"linux"}, \texttt{"solaris"}, 185\texttt{"macosx"} or \texttt{"winNT"}.\footnote{% 186The string \texttt{"winNT"} is used for Microsoft Windows operating systems that are at least as recent as Windows~NT. 187This includes Windows~2000, XP, Vista, Windows~10 \textit{etc}. 188Do not use \texttt{"winNT"} when using Poly/ML \textit{via} Cygwin or the Linux sub-system.} 189 190In extreme circumstances it is possible to edit the file 191\texttt{tools/configure.sml} yourself to set configuration variables 192directly. (If you are using Poly/ML, you must edit 193\texttt{tools-poly/configure.sml} instead.) At the top of this file 194various incomplete SML declarations are present, but commented out. 195You will need to uncomment this section (remove the \texttt{(*} and 196\texttt{*)} markers), and provide sensible values. All strings must 197be enclosed in double quotes. 198 199The \texttt{holdir} value must be the name of the top-level directory 200listed in the first session above. The \texttt{OS} value should be 201one of the strings specified in the accompanying comment. 202 203When working with Poly/ML, the \texttt{poly} string must be the path to the \texttt{poly} executable that begins an interactive \ML{} session. 204The \texttt{polymllibdir} must be a path to a directory that contains the file \texttt{libpolymain.a}. 205When working with Moscow~ML, the \texttt{mosmldir} value must be the 206name of the directory containing the Moscow~ML binaries 207(\texttt{mosmlc}, \texttt{mosml}, \texttt{mosmllex} etc). 208 209Subsequent values (\texttt{CC} and \texttt{GNUMAKE}) are needed for 210``optional'' components of the system. The first gives a string 211suitable for invoking the system's C compiler, and the second 212specifies a \textsf{make} program. 213 214After editing, \texttt{tools/configure.sml} the lines above will look 215something like: 216 217\begin{session} 218\begin{alltt} 219\dol more configure.sml 220 ... 221val mosmldir = "/home/mn200/mosml"; 222val holdir = "/home/mn200/hol"; 223val OS = "linux" (* Operating system; choices are: 224 "linux", "solaris", "unix", "winNT" *) 225 226val CC = "gcc"; (* C compiler (for building quote filter) *) 227val GNUMAKE = "gnumake"; (* for robdd library *) 228 ... 229\dol 230\end{alltt} 231\end{session} 232 233\noindent Now, at either this level (in the \texttt{tools} or 234\texttt{tools-poly} directory) or at the level above, the script 235\texttt{configure.sml} must be piped into the \ML{} interpreter (\ie, 236\texttt{mosml} or \texttt{poly}). For example, 237 238\begin{session} 239\begin{alltt} 240\dol mosml < tools/configure.sml 241Moscow ML version 2.01 (January 2004) 242Enter `quit();' to quit. 243- > val mosmldir = "/home/mn200/mosml" : string 244 val holdir = "/home/mn200/hol" : string 245 val OS = "linux" : string 246- > val CC = "gcc" : string 247 ... 248Beginning configuration. 249- Making bin/Holmake. 250 ... 251Making bin/build. 252- Making hol98-mode.el (for Emacs) 253- Setting up the standard prelude. 254- Setting up src/0/Globals.sml. 255- Generating bin/hol. 256- Generating bin/hol.noquote. 257- Attempting to compile quote filter ... successful. 258- Setting up the muddy library Makefile. 259- Setting up the help Makefile. 260- 261Finished configuration! 262- 263\dol 264\end{alltt} 265\end{session} 266 267 268 269%%% Local Variables: 270%%% mode: latex 271%%% TeX-master: "tutorial" 272%%% End: 273