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