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