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