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;
     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.  See the script
     9 conv-theory-files.pl on directory Tools.
    10 ------------------------------------------------------------------------------
    11 
    12 This directory contains the complete Isabelle system.  To build and test
    13 all the Isabelle object-logics, use the shell script make-all (on directory
    14 Tools).  Pure Isabelle and each of the object-logics can be built
    15 separately using the Makefiles in the respective directories; read them for
    16 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 Tools/make-all-nj for an
    30 example 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 "/bin/sml".
    41 If, after stripping a leading pathname, the compiler begins with the letters
    42 "poly" then the Makefiles assume Poly/ML.  If it begins with the letters "sml"
    43 then they assume 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 Important files include...
    54   COPYRIGHT 	Copyright notice and Disclaimer of Warranty
    55   Pure		contains source files for Pure Isabelle (no object-logic)
    56   Provers	contains generic theorem provers: simplifier, etc.
    57   Tools		contains shell scripts and utilities 
    58 
    59 The following subdirectories contain object-logics:
    60   FOL 	  Natural deduction First-Order Logic (intuitionistic and classical)
    61   FOLP 	  First-Order Logic with Proof terms
    62   ZF	  Zermelo-Fraenkel set theory
    63   HOL	  Classical Higher-Order Logic
    64   LCF     Logic for Computable Functions (domain theory) built upon FOL
    65   HOLCF   A version of LCF built upon HOL
    66   CTT	  Constructive Type Theory
    67   LK	  Classical first-order sequent calculus
    68   Modal	  The modal logics T, S4, S43
    69   CCL	  Martin Coen's Classical Computational Logic
    70   Cube	  Barendregt's Lambda Cube
    71 
    72 David Aspinall has written a user interface for Isabelle.  It runs under
    73 GNU Emacs.  It's useful to both novices and experts.  You can get it by ftp
    74 from ftp.dcs.ed.ac.uk, file /pub/da/Isamode.tar.gz.
    75 
    76 Object-logics include examples files in subdirectory ex or file ex.ML.
    77 These files can be loaded in batch mode.  The commands can also be
    78 executed interactively, using the windows on your workstation.  This is a
    79 good way to get started.
    80 
    81 Each object-logic is built on top of Pure Isabelle, and possibly on top of
    82 another object logic like FOL or LK.  A database or binary called Pure is
    83 first created, then the object-logic is loaded on top.  Poly/ML extends
    84 Pure using its "make_database" operation.  Standard ML of New Jersey starts
    85 with the Pure core image and loads the object-logic's ROOT.ML.
    86 
    87 		HOW TO GET A STANDARD ML COMPILER
    88 
    89 To obtain Poly/ML, contact Mike Crawley <mjc@ahl.co.uk> at Abstract
    90 Hardware Ltd, The Howell Building, Brunel University, Uxbridge UB8 3PH,
    91 England.
    92 
    93 To obtain Standard ML of New Jersey, contact David MacQueen
    94 <dbm@com.att.research> at AT&T Bell Laboratories, 600 Mountain Avenue,
    95 Murray Hill, NJ 07974, USA.  This compiler is available by FTP.  Connect to
    96 research.att.com; login as anonymous with your userid as password; set
    97 binary mode; transfer files from the directory dist/ml.
    98 
    99 ------------------------------------------------------------------------------
   100 
   101 The electronic mailing list isabelle-users@cl.cam.ac.uk provides a forum
   102 for Isabelle users to discuss problems and exchange information.  To join,
   103 send a message to isabelle-users-request@cl.cam.ac.uk.
   104 
   105 ------------------------------------------------------------------------------
   106 
   107 Please report any problems you encounter.  While we shall try to be helpful,
   108 we can accept no responsibility for the deficiences of Isabelle and their
   109 consequences.
   110 
   111 Lawrence C Paulson		E-mail: lcp@cl.cam.ac.uk
   112 Computer Laboratory 		Phone: +44-223-334600
   113 University of Cambridge 	Fax:   +44-223-334748 
   114 Pembroke Street 
   115 Cambridge CB2 3QG 
   116 England
   117 
   118 Tobias Nipkow			E-mail: nipkow@informatik.tu-muenchen.de
   119 Institut für Informatik		Phone: +49-89-2105-2690
   120 T. U. München			Fax:   +49-89-2105-8183
   121 D-80290 München
   122 Germany
   123 
   124 $Id$