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