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