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