forked from HOL-Theorem-Prover/HOL
-
Notifications
You must be signed in to change notification settings - Fork 0
/
INSTALL
198 lines (142 loc) · 7.75 KB
/
INSTALL
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
Getting and building the HOL system
-----------------------------------
Get the HOL sources from SourceForge at http://hol.sourceforge.net
You will also need either:
the Moscow ML compiler (version 2.01) from
http://www.itu.dk/~sestoft/mosml.html
or Poly/ML, from
http://www.polyml.org
Windows users can also build the system by running a self-installing
executable (available from the above http://hol.sourceforge.net). 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. [Moscow ML:] First, install Moscow ML. This is usually
straightforward. The directory where it lives will be called
<mosml-dir> 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. These variables will be
set for you by the latest self-installing executable available
from the Moscow ML home-page.
[Poly/ML:] Install the latest version of Poly/ML. Note that you
will not be able to use the HolBddLib example with this
implementation.
You must ensure that your dynamic library loading picks up
libpolyml.so and libpolymain.so. If these files are in /usr/lib,
you will not have to change anything, but other locations may
require further system configuration (typically done by setting the
LD_LIBRARY_PATH environment variable). A sample LD_LIBRARY_PATH
initialisation command (in a file such as ~/.bashrc) might be
declare -x LD_LIBRARY_PATH=/usr/local/lib:$HOME/lib
Do not use the --with-portable option.
B. Unpack HOL with the commands
gunzip release.tar.gz; tar xf release.tar
in Unix, or the appropriate clicking activity in Windows (use a
program like Winzip). The resulting directory will be called
<hol-dir> in the following. When fully built, <hol-dir> takes
approximately 35M of disk space, so be sure you have enough before
starting.
C. In the HOL directory (<hol-dir>), type
[Moscow ML:] mosml < tools/smart-configure.sml
[Poly/ML:] poly < tools/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
[Moscow ML:] config-override in <hol-dir>
[Poly/ML:] poly-includes.ML in <hol-dir>/tools-poly
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. Most parameters must be given as ML strings, while
dynlib_available must be an ML boolean (either true or false). The
value for mosmldir must be the directory containing the Moscow ML
executables (mosml, mosmlc, etc). The value for poly must be the
path to the poly executable.
The valid values for OS are "linux", "unix", "solaris", "macosx"
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", "Windows XP" and "Windows Vista".
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:
[Moscow ML:] <hol-dir>/bin/build
[Poly/ML:] <hol-dir>/bin/build
This builds the system. In case of difficulty, the configuration
can be gone through by hand, by starting the ML interpreter and
stepping through [Moscow ML:] tools/configure.sml, [Poly/ML:]
tools-poly/configure.sml by hand. Similarly, the execution of
build.sml can also be stepped through in the interpreter. This can
be somewhat time-consuming, but will help pinpoint any problems.
On Windows, the system ends up creating two copies of every object
file. 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 (it takes a while!), successfully, you are
done. From <hol-dir> you can now access
bin/hol * The standard HOL interactive system
bin/hol.noquote * The interactive system with quote
preprocessing turned off
bin/hol.bare * A "stripped down" version of hol
bin/hol.bare.noquote * A "stripped down" version of hol.noquote,
with quote preprocessing turned off
bin/Holmake * A batch compiler for HOL directories
src/ * System sources
examples/ * Examples of the use of the system
On Windows the hol scripts additionally include a .bat extension,
and Holmake has a .exe extension.
At this point, the system is build in <hol-dir> and cannot easily
be moved to other locations. In other words, you should unpack HOL
in the location/directory where you wish to access it for all your
future work.
External tools
--------------
The HOL installation currently includes a C library (in HolBddLib),
the C sources for the SMV model-checker (in temporalLib), and for a
SAT solver (minisat) in HolSat. Building these under Unix requires a
C compiler to have been specified in tools/configure.sml. Under
Windows, precompiled binaries are available for the C library and for
minisat.
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. Please include the following details:
. hardware/OS the build failed on
. version of Moscow ML or Poly/ML being used
. version of HOL being built
* Alternatively, use the github issues web-page at
http://github.com/mn200/HOL/issues
and submit a description of the problem.
* If a build attempt fails for some reason, you should attempt to invoke
bin/build -cleanAll
from <hol-dir> before a new build attempt.