README
author lcp
Tue Jul 12 18:38:39 1994 +0200 (1994-07-12)
changeset 470 6cb6dd05d761
parent 370 e95e212512d1
child 609 6d520505e704
permissions -rw-r--r--
minor updates
lcp@86
     1
		     ISABELLE-93 DISTRIBUTION DIRECTORY
clasohm@0
     2
clasohm@0
     3
------------------------------------------------------------------------------
lcp@86
     4
ISABELLE-93 IS INCOMPATIBLE WITH EARLIER VERSIONS.  PLEASE CONSULT THE
clasohm@0
     5
DOCUMENTATION.
clasohm@0
     6
------------------------------------------------------------------------------
clasohm@0
     7
clasohm@0
     8
This directory contains the complete Isabelle system.  To build and test the
clasohm@0
     9
entire system, including all object-logics, use the shell script make-all.
clasohm@0
    10
Pure Isabelle and each of the object-logics can be built separately using the
clasohm@0
    11
Makefiles in the respective directories; read them for more information.
clasohm@0
    12
clasohm@0
    13
				THE MAKEFILES
clasohm@0
    14
clasohm@0
    15
The Makefiles can use two different Standard ML compilers: Poly/ML version
lcp@86
    16
2.03 or later (from Abstract Hardware Ltd) and Standard ML of New Jersey
lcp@86
    17
(Version 0.93 or later).  Poly/ML is a commercial product and costs money,
clasohm@0
    18
but it is reliable and its database system is convenient for interactive
lcp@196
    19
work.  SML of New Jersey requires lots of store and disc space, but it is
clasohm@0
    20
free and its code sometimes runs faster.  Both compilers are perfectly
clasohm@0
    21
satisfactory for running Isabelle.
clasohm@0
    22
lcp@370
    23
The Makefiles and make-all use environment variables that you should set
lcp@370
    24
according to your site configuration.  See file make-all-nj for an example
lcp@370
    25
using the Bourne shell, sh.
clasohm@0
    26
clasohm@0
    27
ISABELLEBIN is the directory to hold Poly/ML databases or New Jersey ML
lcp@470
    28
images.  This directory *must* be different from the Isabelle source
lcp@470
    29
directory.  When using Poly/ML, ISABELLEBIN must be an absolute pathname
lcp@470
    30
(one starting with "/").
clasohm@0
    31
lcp@470
    32
ML_DBASE is an *absolute* pathname to the initial Poly/ML database.  It is not
lcp@470
    33
required for New Jersey ML.
clasohm@0
    34
clasohm@0
    35
ISABELLECOMP is the ML compiler, typically "poly -noDisplay" or "sml".  If
clasohm@0
    36
ISABELLECOMP begins with the letters "poly" then the Makefiles assume that
clasohm@0
    37
it is Poly/ML; if it begins with the letters "sml" then they assume
lcp@86
    38
Standard ML of New Jersey.  
lcp@86
    39
lcp@86
    40
If a Poly/ML session fails with the message "Run out of store" then you
lcp@86
    41
have used up the entire heap.  If your tactic is not in a loop, allocating
lcp@86
    42
more heap at startup should correct the problem.  For instance, "poly -h
lcp@86
    43
15000" allocates sufficient heap space to rebuild all Isabelle examples.
clasohm@0
    44
clasohm@0
    45
clasohm@0
    46
			 STRUCTURE OF THIS DIRECTORY
clasohm@0
    47
clasohm@0
    48
The directory Pure containes pure Isabelle, which has no object-logic.
clasohm@0
    49
clasohm@0
    50
Other important files include...
lcp@86
    51
  COPYRIGHT   		Copyright notice and Disclaimer of Warranty
lcp@86
    52
  make-all		shell script for building entire system
lcp@370
    53
  make-all-poly		sample make-all invocation for Poly/ML
lcp@370
    54
  make-all-nj		sample make-all invocation for SML of NJ
lcp@93
    55
  change_simp		shell script to help convert sources to new simplifier
lcp@470
    56
  conv-theory-files.pl  perl script to rename old theory files
lcp@86
    57
  expandshort		shell script to expand "shortcuts" in files
lcp@86
    58
  prove_goal.el       	Emacs command to change proof format
lcp@86
    59
  xlisten		shell script for running Isabelle under X
lcp@86
    60
  teeinput		shell script to run Isabelle, logging inputs to a file
lcp@86
    61
  Pure			directory of source files for Pure Isabelle
lcp@86
    62
  Provers		directory of generic theorem provers
clasohm@0
    63
clasohm@0
    64
xlisten sets up a window running Isabelle, with a separate small "listener"
clasohm@0
    65
window, which keeps a log of all input lines.  This log is a useful record
clasohm@0
    66
of a session.  If you are not running X windows, teeinput can still be used at
clasohm@0
    67
least to record (if not to display) the log.
clasohm@0
    68
clasohm@0
    69
The following subdirectories contain object-logics:
lcp@86
    70
  FOL 	  Natural deduction First-Order Logic (intuitionistic and classical)
lcp@86
    71
  FOLP 	  First-Order Logic with Proof terms
lcp@86
    72
  ZF	  Zermelo-Fraenkel set theory
lcp@370
    73
  HOL	  Classical Higher-Order Logic
lcp@370
    74
  LCF     Logic for Computable Functions (domain theory) built upon FOL
lcp@370
    75
  HOLCF   A version of LCF built upon HOL
lcp@86
    76
  CTT	  Constructive Type Theory
lcp@86
    77
  LK	  Classical first-order sequent calculus
lcp@86
    78
  Modal	  The modal logics T, S4, S43
lcp@86
    79
  CCL	  Martin Coen's Classical Computational Logic
lcp@86
    80
  Cube	  Barendregt's Lambda Cube
clasohm@0
    81
clasohm@0
    82
Object-logics include examples files in subdirectory ex or file ex.ML.
clasohm@0
    83
These files can be loaded in batch mode.  The commands can also be
clasohm@0
    84
executed interactively, using the windows on your workstation.  This is a
clasohm@0
    85
good way to get started.
clasohm@0
    86
clasohm@0
    87
Each object-logic is built on top of Pure Isabelle, and possibly on top of
lcp@196
    88
another object logic like FOL or LK.  A database or binary called Pure is
clasohm@0
    89
first created, then the object-logic is loaded on top.  Poly/ML extends
clasohm@0
    90
Pure using its "make_database" operation.  Standard ML of New Jersey starts
clasohm@0
    91
with the Pure core image and loads the object-logic's ROOT.ML.
clasohm@0
    92
clasohm@0
    93
		HOW TO GET A STANDARD ML COMPILER
clasohm@0
    94
clasohm@0
    95
To obtain Poly/ML, contact Mike Crawley <mjc@ahl.co.uk> at Abstract
clasohm@0
    96
Hardware Ltd, The Howell Building, Brunel University, Uxbridge UB8 3PH,
clasohm@0
    97
England.
clasohm@0
    98
clasohm@0
    99
To obtain Standard ML of New Jersey, contact David MacQueen
clasohm@0
   100
<dbm@com.att.research> at AT&T Bell Laboratories, 600 Mountain Avenue,
clasohm@0
   101
Murray Hill, NJ 07974, USA.  This compiler is available by FTP.  Connect to
clasohm@0
   102
research.att.com; login as anonymous with your userid as password; set
clasohm@0
   103
binary mode; transfer files from the directory dist/ml.
clasohm@0
   104
clasohm@0
   105
------------------------------------------------------------------------------
clasohm@0
   106
lcp@196
   107
The electronic mailing list isabelle-users@cl.cam.ac.uk provides a forum
lcp@196
   108
for Isabelle users to discuss problems and exchange information.  To join,
lcp@196
   109
send a message to isabelle-users-request@cl.cam.ac.uk.
lcp@196
   110
lcp@196
   111
------------------------------------------------------------------------------
lcp@196
   112
lcp@93
   113
Please report any problems you encounter.  While we shall try to be helpful,
lcp@93
   114
we can accept no responsibility for the deficiences of Isabelle and their
clasohm@0
   115
consequences.
clasohm@0
   116
clasohm@0
   117
Lawrence C Paulson		E-mail: lcp@cl.cam.ac.uk
clasohm@0
   118
Computer Laboratory 		Phone: +44-223-334600
clasohm@0
   119
University of Cambridge 	Fax:   +44-223-334748 
clasohm@0
   120
Pembroke Street 
clasohm@0
   121
Cambridge CB2 3QG 
clasohm@0
   122
England
clasohm@0
   123
clasohm@0
   124
Tobias Nipkow			E-mail: nipkow@informatik.tu-muenchen.de
clasohm@0
   125
Institut fuer Informatik	Phone: +49-89-2105-2690
clasohm@0
   126
T. U. Muenchen			Fax:   +49-89-2105-8183
nipkow@94
   127
D-80290 Muenchen
clasohm@0
   128
Germany
clasohm@0
   129
lcp@470
   130
Last updated 20 May 1994