author | wenzelm |
Mon, 18 Nov 1996 17:27:59 +0100 | |
changeset 2195 | e8271379ba4b |
parent 2189 | c00533aec02f |
child 2213 | a96a7b6c0437 |
permissions | -rw-r--r-- |
609 | 1 |
ISABELLE-94 DISTRIBUTION DIRECTORY |
0 | 2 |
|
3 |
------------------------------------------------------------------------------ |
|
609 | 4 |
ISABELLE-94 IS INCOMPATIBLE WITH EARLIER VERSIONS. PLEASE CONSULT THE |
5 |
DOCUMENTATION. |
|
6 |
||
7 |
In particular, theory files are no longer forced into lower case, but must |
|
816 | 8 |
be identical to the actual theory name. See the script |
9 |
conv-theory-files.pl on directory Tools. |
|
0 | 10 |
------------------------------------------------------------------------------ |
11 |
||
816 | 12 |
This directory contains the complete Isabelle system. To build and test |
13 |
all the Isabelle object-logics, use the shell script make-all (on directory |
|
14 |
Tools). Pure Isabelle and each of the object-logics can be built |
|
15 |
separately using the Makefiles in the respective directories; read them for |
|
16 |
more information. |
|
0 | 17 |
|
2189 | 18 |
HOW TO BUILD ISABELLE |
19 |
||
20 |
Here are brief instructions. For more detail, read further. |
|
21 |
||
22 |
1. Create a directory to hold the Isabelle executable images, and |
|
23 |
set the environment variable ISABELLEBIN to its pathname. |
|
24 |
||
25 |
2. Set the environment variable ISABELLECOMP to the command to execute your |
|
26 |
Standard ML compiler. |
|
27 |
||
28 |
3. If using Poly/ML, set the environment variable ML_DBASE to the pathname |
|
29 |
of the empty Poly/ML database. |
|
30 |
||
31 |
4. Change your working directory to that containing this file. |
|
32 |
||
33 |
5a. To build ALL logics and run examples, type "make-all" and wait up to |
|
34 |
10 hours. Standard ML of New Jersey will require up to 200M |
|
35 |
of disc space! Poly/ML will require about 25M. |
|
36 |
||
37 |
-OR- |
|
38 |
5b. To build ALL logics but run no examples, type "make-all -notest". This |
|
39 |
is much faster than 5a but needs just as much disc space. |
|
0 | 40 |
|
2189 | 41 |
-OR- |
42 |
5c. To build just one logic, such as HOL, change to directory HOL and type |
|
43 |
"make" or "make test". This may trigger further Makes automatically. |
|
44 |
||
45 |
||
46 |
SUITABLE ML COMPILERS |
|
47 |
||
48 |
You use two different Standard ML compilers: Poly/ML version 2.03 or later |
|
49 |
(from Abstract Hardware Ltd) and Standard ML of New Jersey (Version 0.93 or |
|
50 |
later). Poly/ML is a commercial product and costs money, but it is stable and |
|
51 |
efficient; moreover its database system is convenient for interactive work. |
|
52 |
SML of New Jersey requires lots of store and disc space, but it is free and |
|
53 |
its code sometimes runs faster. Both compilers are perfectly satisfactory for |
|
54 |
running Isabelle. |
|
55 |
||
56 |
To obtain Poly/ML, contact Abstract Hardware Ltd, The Howell Building, Brunel |
|
57 |
University, Uxbridge UB8 3PH, England, email lambda@ahl.co.uk. |
|
58 |
||
59 |
To obtain Standard ML of New Jersey, see the Web page |
|
60 |
http://cm.bell-labs.com/cm/cs/what/smlnj/software.html |
|
61 |
or send email to sml-nj@research.bell-labs.com. |
|
62 |
||
63 |
||
64 |
ENVIRONMENT VARIABLES |
|
0 | 65 |
|
370
e95e212512d1
make-all-poly, make-all-nj: restored to main directory as examples
lcp
parents:
196
diff
changeset
|
66 |
The Makefiles and make-all use environment variables that you should set |
816 | 67 |
according to your site configuration. See file Tools/make-all-nj for an |
68 |
example using the Bourne shell, sh. |
|
0 | 69 |
|
70 |
ISABELLEBIN is the directory to hold Poly/ML databases or New Jersey ML |
|
470 | 71 |
images. This directory *must* be different from the Isabelle source |
72 |
directory. When using Poly/ML, ISABELLEBIN must be an absolute pathname |
|
73 |
(one starting with "/"). |
|
0 | 74 |
|
470 | 75 |
ML_DBASE is an *absolute* pathname to the initial Poly/ML database. It is not |
76 |
required for New Jersey ML. |
|
0 | 77 |
|
2189 | 78 |
ISABELLECOMP is the command to run ML compiler, typically "/bin/sml" or "poly |
79 |
-noDisplay -h 15000". (The -h switch to Poly specifies an initial heap |
|
80 |
allocation, which you should consider increasing if a command fails with the |
|
81 |
message "Run out of store".) |
|
82 |
||
2119
1d8ae796f3bf
Mentions the possibility of pathnames in ISABELLECOMP;
paulson
parents:
869
diff
changeset
|
83 |
If, after stripping a leading pathname, the compiler begins with the letters |
1d8ae796f3bf
Mentions the possibility of pathnames in ISABELLECOMP;
paulson
parents:
869
diff
changeset
|
84 |
"poly" then the Makefiles assume Poly/ML. If it begins with the letters "sml" |
1d8ae796f3bf
Mentions the possibility of pathnames in ISABELLECOMP;
paulson
parents:
869
diff
changeset
|
85 |
then they assume Standard ML of New Jersey. |
86 | 86 |
|
0 | 87 |
|
88 |
STRUCTURE OF THIS DIRECTORY |
|
89 |
||
816 | 90 |
Important files include... |
91 |
COPYRIGHT Copyright notice and Disclaimer of Warranty |
|
92 |
Pure contains source files for Pure Isabelle (no object-logic) |
|
93 |
Provers contains generic theorem provers: simplifier, etc. |
|
869 | 94 |
Tools contains shell scripts and utilities |
0 | 95 |
|
96 |
The following subdirectories contain object-logics: |
|
2189 | 97 |
FOL natural deduction First-Order Logic |
98 |
(intuitionistic and classical versions) |
|
99 |
FOLP First-Order Logic with Proof terms |
|
100 |
ZF Zermelo-Fraenkel set theory |
|
101 |
HOL Classical Higher-Order Logic |
|
102 |
LCF Logic for Computable Functions (domain theory) built upon FOL |
|
103 |
HOLCF A version of LCF built upon HOL |
|
104 |
CTT Constructive Type Theory |
|
105 |
Sequents Sequent calcul: first-order logic |
|
106 |
modal logics T, S4, S43 |
|
107 |
intuitionistic linear logic |
|
108 |
CCL Martin Coen's Classical Computational Logic |
|
109 |
Cube Barendregt's Lambda Cube |
|
0 | 110 |
|
816 | 111 |
David Aspinall has written a user interface for Isabelle. It runs under |
112 |
GNU Emacs. It's useful to both novices and experts. You can get it by ftp |
|
113 |
from ftp.dcs.ed.ac.uk, file /pub/da/Isamode.tar.gz. |
|
114 |
||
0 | 115 |
Object-logics include examples files in subdirectory ex or file ex.ML. |
116 |
These files can be loaded in batch mode. The commands can also be |
|
117 |
executed interactively, using the windows on your workstation. This is a |
|
118 |
good way to get started. |
|
119 |
||
120 |
Each object-logic is built on top of Pure Isabelle, and possibly on top of |
|
2189 | 121 |
another object logic like FOL or HOL. A database or binary called Pure is |
0 | 122 |
first created, then the object-logic is loaded on top. Poly/ML extends |
123 |
Pure using its "make_database" operation. Standard ML of New Jersey starts |
|
124 |
with the Pure core image and loads the object-logic's ROOT.ML. |
|
125 |
||
126 |
------------------------------------------------------------------------------ |
|
127 |
||
196 | 128 |
The electronic mailing list isabelle-users@cl.cam.ac.uk provides a forum |
129 |
for Isabelle users to discuss problems and exchange information. To join, |
|
130 |
send a message to isabelle-users-request@cl.cam.ac.uk. |
|
131 |
||
132 |
------------------------------------------------------------------------------ |
|
133 |
||
93 | 134 |
Please report any problems you encounter. While we shall try to be helpful, |
135 |
we can accept no responsibility for the deficiences of Isabelle and their |
|
0 | 136 |
consequences. |
137 |
||
138 |
Lawrence C Paulson E-mail: lcp@cl.cam.ac.uk |
|
139 |
Computer Laboratory Phone: +44-223-334600 |
|
140 |
University of Cambridge Fax: +44-223-334748 |
|
141 |
Pembroke Street |
|
142 |
Cambridge CB2 3QG |
|
143 |
England |
|
144 |
||
145 |
Tobias Nipkow E-mail: nipkow@informatik.tu-muenchen.de |
|
609 | 146 |
Institut für Informatik Phone: +49-89-2105-2690 |
147 |
T. U. München Fax: +49-89-2105-8183 |
|
148 |
D-80290 München |
|
0 | 149 |
Germany |
150 |
||
609 | 151 |
$Id$ |