1 ISABELLE-94 DISTRIBUTION DIRECTORY |
|
2 |
|
3 ------------------------------------------------------------------------------ |
|
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 |
|
8 be identical to the actual theory name. See the script |
|
9 conv-theory-files.pl on directory Tools. |
|
10 ------------------------------------------------------------------------------ |
|
11 |
|
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. |
|
17 |
|
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. |
|
23 Set the environment variable ISABELLEBIN to its full (absolute) 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 full |
|
29 pathname 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. |
|
40 |
|
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 can 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/NJ needs lots of store and disc space, but it is free. Some recent |
|
53 versions of SML/NJ are significantly faster than 0.93, but beware of many |
|
54 incompatibilities among them; you might be forced to edit the file |
|
55 Pure/NJ1xx.ML. VERSIONS BETWEEN 109.16 AND 109.21 ARE VERY SLOW. |
|
56 |
|
57 To obtain Poly/ML, contact Abstract Hardware Ltd, The Howell Building, Brunel |
|
58 University, Uxbridge UB8 3PH, England, email lambda@ahl.co.uk. |
|
59 |
|
60 To obtain Standard ML of New Jersey, see the Web page |
|
61 http://cm.bell-labs.com/cm/cs/what/smlnj/software.html |
|
62 or send email to sml-nj@research.bell-labs.com. |
|
63 |
|
64 |
|
65 ENVIRONMENT VARIABLES |
|
66 |
|
67 The Makefiles and make-all use environment variables that you should set |
|
68 according to your site configuration. See file Tools/make-all-nj for an |
|
69 example using the Bourne shell, sh. |
|
70 |
|
71 ISABELLEBIN is the directory to hold Poly/ML databases or New Jersey ML |
|
72 images. This directory *must* be different from the Isabelle source |
|
73 directory. ISABELLEBIN must be an absolute pathname (one starting with "/"). |
|
74 |
|
75 ML_DBASE is an *absolute* pathname to the initial Poly/ML database. It is not |
|
76 required for New Jersey ML. |
|
77 |
|
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".) Please DO NOT use a command such as |
|
82 "sml @SMLdebug=/dev/null", since the pathname after "sml" will confuse the |
|
83 Makefiles. |
|
84 |
|
85 If, after stripping a leading pathname, the compiler begins with the letters |
|
86 "poly" then the Makefiles assume Poly/ML. If it begins with the letters "sml" |
|
87 then they assume Standard ML of New Jersey. |
|
88 |
|
89 |
|
90 STRUCTURE OF THIS DIRECTORY |
|
91 |
|
92 Important files include... |
|
93 COPYRIGHT Copyright notice and Disclaimer of Warranty |
|
94 Pure contains source files for Pure Isabelle (no object-logic) |
|
95 Provers contains generic theorem provers: simplifier, etc. |
|
96 Tools contains shell scripts and utilities |
|
97 |
|
98 The following subdirectories contain object-logics: |
|
99 FOL natural deduction First-Order Logic |
|
100 (intuitionistic and classical versions) |
|
101 FOLP First-Order Logic with Proof terms |
|
102 ZF Zermelo-Fraenkel set theory |
|
103 HOL Classical Higher-Order Logic |
|
104 LCF Logic for Computable Functions (domain theory) built upon FOL |
|
105 HOLCF A version of LCF built upon HOL |
|
106 CTT Constructive Type Theory |
|
107 Sequents Sequent calcul: first-order logic |
|
108 modal logics T, S4, S43 |
|
109 intuitionistic linear logic |
|
110 CCL Martin Coen's Classical Computational Logic |
|
111 Cube Barendregt's Lambda Cube |
|
112 |
|
113 David Aspinall has written a user interface for Isabelle. It runs under |
|
114 GNU Emacs. It's useful to both novices and experts. You can get it by ftp |
|
115 from ftp.dcs.ed.ac.uk, file /pub/da/Isamode.tar.gz. |
|
116 |
|
117 Object-logics include examples files in subdirectory ex or file ex.ML. |
|
118 These files can be loaded in batch mode. The commands can also be |
|
119 executed interactively, using the windows on your workstation. This is a |
|
120 good way to get started. |
|
121 |
|
122 Each object-logic is built on top of Pure Isabelle, and possibly on top of |
|
123 another object logic like FOL or HOL. A database or binary called Pure is |
|
124 first created, then the object-logic is loaded on top. Poly/ML extends |
|
125 Pure using its "make_database" operation. Standard ML of New Jersey starts |
|
126 with the Pure core image and loads the object-logic's ROOT.ML. |
|
127 |
|
128 ------------------------------------------------------------------------------ |
|
129 |
|
130 The electronic mailing list isabelle-users@cl.cam.ac.uk provides a forum |
|
131 for Isabelle users to discuss problems and exchange information. To join, |
|
132 send a message to isabelle-users-request@cl.cam.ac.uk. |
|
133 |
|
134 ------------------------------------------------------------------------------ |
|
135 |
|
136 Please report any problems you encounter. While we shall try to be helpful, |
|
137 we can accept no responsibility for the deficiences of Isabelle and their |
|
138 consequences. |
|
139 |
|
140 Lawrence C Paulson E-mail: lcp@cl.cam.ac.uk |
|
141 Computer Laboratory Phone: +44-223-334600 |
|
142 University of Cambridge Fax: +44-223-334748 |
|
143 Pembroke Street |
|
144 Cambridge CB2 3QG |
|
145 England |
|
146 |
|
147 Tobias Nipkow E-mail: nipkow@informatik.tu-muenchen.de |
|
148 Institut für Informatik Phone: +49-89-2105-2690 |
|
149 T. U. München Fax: +49-89-2105-8183 |
|
150 D-80290 München |
|
151 Germany |
|
152 |
|
153 $Id$ |
|