README
author paulson
Mon Oct 21 11:37:21 1996 +0200 (1996-10-21)
changeset 2119 1d8ae796f3bf
parent 869 242b5050c1a6
child 2189 c00533aec02f
permissions -rw-r--r--
Mentions the possibility of pathnames in ISABELLECOMP;
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
clasohm@0
    18
				THE MAKEFILES
clasohm@0
    19
clasohm@0
    20
The Makefiles can use two different Standard ML compilers: Poly/ML version
lcp@86
    21
2.03 or later (from Abstract Hardware Ltd) and Standard ML of New Jersey
lcp@86
    22
(Version 0.93 or later).  Poly/ML is a commercial product and costs money,
clasohm@0
    23
but it is reliable and its database system is convenient for interactive
lcp@196
    24
work.  SML of New Jersey requires lots of store and disc space, but it is
clasohm@0
    25
free and its code sometimes runs faster.  Both compilers are perfectly
clasohm@0
    26
satisfactory for running Isabelle.
clasohm@0
    27
lcp@370
    28
The Makefiles and make-all use environment variables that you should set
lcp@816
    29
according to your site configuration.  See file Tools/make-all-nj for an
lcp@816
    30
example using the Bourne shell, sh.
clasohm@0
    31
clasohm@0
    32
ISABELLEBIN is the directory to hold Poly/ML databases or New Jersey ML
lcp@470
    33
images.  This directory *must* be different from the Isabelle source
lcp@470
    34
directory.  When using Poly/ML, ISABELLEBIN must be an absolute pathname
lcp@470
    35
(one starting with "/").
clasohm@0
    36
lcp@470
    37
ML_DBASE is an *absolute* pathname to the initial Poly/ML database.  It is not
lcp@470
    38
required for New Jersey ML.
clasohm@0
    39
paulson@2119
    40
ISABELLECOMP is the ML compiler, typically "poly -noDisplay" or "/bin/sml".
paulson@2119
    41
If, after stripping a leading pathname, the compiler begins with the letters
paulson@2119
    42
"poly" then the Makefiles assume Poly/ML.  If it begins with the letters "sml"
paulson@2119
    43
then they assume Standard ML of New Jersey.
lcp@86
    44
lcp@86
    45
If a Poly/ML session fails with the message "Run out of store" then you
lcp@86
    46
have used up the entire heap.  If your tactic is not in a loop, allocating
lcp@86
    47
more heap at startup should correct the problem.  For instance, "poly -h
lcp@86
    48
15000" allocates sufficient heap space to rebuild all Isabelle examples.
clasohm@0
    49
clasohm@0
    50
clasohm@0
    51
			 STRUCTURE OF THIS DIRECTORY
clasohm@0
    52
lcp@816
    53
Important files include...
lcp@816
    54
  COPYRIGHT 	Copyright notice and Disclaimer of Warranty
lcp@816
    55
  Pure		contains source files for Pure Isabelle (no object-logic)
lcp@816
    56
  Provers	contains generic theorem provers: simplifier, etc.
lcp@869
    57
  Tools		contains shell scripts and utilities 
clasohm@0
    58
clasohm@0
    59
The following subdirectories contain object-logics:
lcp@86
    60
  FOL 	  Natural deduction First-Order Logic (intuitionistic and classical)
lcp@86
    61
  FOLP 	  First-Order Logic with Proof terms
lcp@86
    62
  ZF	  Zermelo-Fraenkel set theory
lcp@370
    63
  HOL	  Classical Higher-Order Logic
lcp@370
    64
  LCF     Logic for Computable Functions (domain theory) built upon FOL
lcp@370
    65
  HOLCF   A version of LCF built upon HOL
lcp@86
    66
  CTT	  Constructive Type Theory
lcp@86
    67
  LK	  Classical first-order sequent calculus
lcp@86
    68
  Modal	  The modal logics T, S4, S43
lcp@86
    69
  CCL	  Martin Coen's Classical Computational Logic
lcp@86
    70
  Cube	  Barendregt's Lambda Cube
clasohm@0
    71
lcp@816
    72
David Aspinall has written a user interface for Isabelle.  It runs under
lcp@816
    73
GNU Emacs.  It's useful to both novices and experts.  You can get it by ftp
lcp@816
    74
from ftp.dcs.ed.ac.uk, file /pub/da/Isamode.tar.gz.
lcp@816
    75
clasohm@0
    76
Object-logics include examples files in subdirectory ex or file ex.ML.
clasohm@0
    77
These files can be loaded in batch mode.  The commands can also be
clasohm@0
    78
executed interactively, using the windows on your workstation.  This is a
clasohm@0
    79
good way to get started.
clasohm@0
    80
clasohm@0
    81
Each object-logic is built on top of Pure Isabelle, and possibly on top of
lcp@196
    82
another object logic like FOL or LK.  A database or binary called Pure is
clasohm@0
    83
first created, then the object-logic is loaded on top.  Poly/ML extends
clasohm@0
    84
Pure using its "make_database" operation.  Standard ML of New Jersey starts
clasohm@0
    85
with the Pure core image and loads the object-logic's ROOT.ML.
clasohm@0
    86
clasohm@0
    87
		HOW TO GET A STANDARD ML COMPILER
clasohm@0
    88
clasohm@0
    89
To obtain Poly/ML, contact Mike Crawley <mjc@ahl.co.uk> at Abstract
clasohm@0
    90
Hardware Ltd, The Howell Building, Brunel University, Uxbridge UB8 3PH,
clasohm@0
    91
England.
clasohm@0
    92
clasohm@0
    93
To obtain Standard ML of New Jersey, contact David MacQueen
clasohm@0
    94
<dbm@com.att.research> at AT&T Bell Laboratories, 600 Mountain Avenue,
clasohm@0
    95
Murray Hill, NJ 07974, USA.  This compiler is available by FTP.  Connect to
clasohm@0
    96
research.att.com; login as anonymous with your userid as password; set
clasohm@0
    97
binary mode; transfer files from the directory dist/ml.
clasohm@0
    98
clasohm@0
    99
------------------------------------------------------------------------------
clasohm@0
   100
lcp@196
   101
The electronic mailing list isabelle-users@cl.cam.ac.uk provides a forum
lcp@196
   102
for Isabelle users to discuss problems and exchange information.  To join,
lcp@196
   103
send a message to isabelle-users-request@cl.cam.ac.uk.
lcp@196
   104
lcp@196
   105
------------------------------------------------------------------------------
lcp@196
   106
lcp@93
   107
Please report any problems you encounter.  While we shall try to be helpful,
lcp@93
   108
we can accept no responsibility for the deficiences of Isabelle and their
clasohm@0
   109
consequences.
clasohm@0
   110
clasohm@0
   111
Lawrence C Paulson		E-mail: lcp@cl.cam.ac.uk
clasohm@0
   112
Computer Laboratory 		Phone: +44-223-334600
clasohm@0
   113
University of Cambridge 	Fax:   +44-223-334748 
clasohm@0
   114
Pembroke Street 
clasohm@0
   115
Cambridge CB2 3QG 
clasohm@0
   116
England
clasohm@0
   117
clasohm@0
   118
Tobias Nipkow			E-mail: nipkow@informatik.tu-muenchen.de
lcp@609
   119
Institut für Informatik		Phone: +49-89-2105-2690
lcp@609
   120
T. U. München			Fax:   +49-89-2105-8183
lcp@609
   121
D-80290 München
clasohm@0
   122
Germany
clasohm@0
   123
lcp@609
   124
$Id$