README
author wenzelm
Wed Mar 05 13:37:16 1997 +0100 (1997-03-05)
changeset 2730 865995b744f5
parent 2249 2af17dd5479e
permissions -rw-r--r--
*** empty log message ***
     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 			HOW TO BUILD ISABELLE
    19 
    20 Here are brief instructions.  For more detail, read further.
    21 
    22 1.  Create a directory to hold the Isabelle executable images.
    23     Set the environment variable ISABELLEBIN to its full (absolute) pathname.
    24 
    25 2.  Set the environment variable ISABELLECOMP to the command to execute your
    26     Standard ML compiler.
    27 
    28 3.  If using Poly/ML, set the environment variable ML_DBASE to the full 
    29     pathname of the empty Poly/ML database.
    30 
    31 4.  Change your working directory to that containing this file.
    32 
    33 5a. To build ALL logics and run examples, type "make-all" and wait up to 
    34     10 hours.  Standard ML of New Jersey will require up to 200M
    35     of disc space!  Poly/ML will require about 25M.
    36 
    37 -OR-
    38 5b. To build ALL logics but run no examples, type "make-all -notest".  This
    39     is much faster than 5a but needs just as much disc space.
    40 
    41 -OR-
    42 5c. To build just one logic, such as HOL, change to directory HOL and type
    43     "make" or "make test".  This may trigger further Makes automatically.
    44 
    45 
    46 			SUITABLE ML COMPILERS
    47 
    48 You can use two different Standard ML compilers: Poly/ML version 2.03 or later
    49 (from Abstract Hardware Ltd) and Standard ML of New Jersey (Version 0.93 or
    50 later).  Poly/ML is a commercial product and costs money, but it is stable and
    51 efficient; moreover its database system is convenient for interactive work.
    52 SML/NJ needs lots of store and disc space, but it is free.  Some recent
    53 versions of SML/NJ are significantly faster than 0.93, but beware of many
    54 incompatibilities among them; you might be forced to edit the file
    55 Pure/NJ1xx.ML.  VERSIONS BETWEEN 109.16 AND 109.21 ARE VERY SLOW.
    56 
    57 To obtain Poly/ML, contact Abstract Hardware Ltd, The Howell Building, Brunel
    58 University, Uxbridge UB8 3PH, England, email lambda@ahl.co.uk.
    59 
    60 To obtain Standard ML of New Jersey, see the Web page 
    61 	http://cm.bell-labs.com/cm/cs/what/smlnj/software.html
    62 or send email to sml-nj@research.bell-labs.com.
    63 
    64 
    65 			ENVIRONMENT VARIABLES
    66 
    67 The Makefiles and make-all use environment variables that you should set
    68 according to your site configuration.  See file Tools/make-all-nj for an
    69 example using the Bourne shell, sh.
    70 
    71 ISABELLEBIN is the directory to hold Poly/ML databases or New Jersey ML
    72 images.  This directory *must* be different from the Isabelle source
    73 directory.  ISABELLEBIN must be an absolute pathname (one starting with "/").
    74 
    75 ML_DBASE is an *absolute* pathname to the initial Poly/ML database.  It is not
    76 required for New Jersey ML.
    77 
    78 ISABELLECOMP is the command to run ML compiler, typically "/bin/sml" or "poly
    79 -noDisplay -h 15000".  (The -h switch to Poly specifies an initial heap
    80 allocation, which you should consider increasing if a command fails with the
    81 message "Run out of store".)  Please DO NOT use a command such as
    82 "sml @SMLdebug=/dev/null", since the pathname after "sml" will confuse the
    83 Makefiles. 
    84 
    85 If, after stripping a leading pathname, the compiler begins with the letters
    86 "poly" then the Makefiles assume Poly/ML.  If it begins with the letters "sml"
    87 then they assume Standard ML of New Jersey.
    88 
    89 
    90 			 STRUCTURE OF THIS DIRECTORY
    91 
    92 Important files include...
    93   COPYRIGHT 	Copyright notice and Disclaimer of Warranty
    94   Pure		contains source files for Pure Isabelle (no object-logic)
    95   Provers	contains generic theorem provers: simplifier, etc.
    96   Tools		contains shell scripts and utilities 
    97 
    98 The following subdirectories contain object-logics:
    99   FOL 		natural deduction First-Order Logic 
   100 			(intuitionistic and classical versions)
   101   FOLP 		First-Order Logic with Proof terms
   102   ZF		Zermelo-Fraenkel set theory
   103   HOL		Classical Higher-Order Logic
   104   LCF		Logic for Computable Functions (domain theory) built upon FOL
   105   HOLCF		A version of LCF built upon HOL
   106   CTT		Constructive Type Theory
   107   Sequents	Sequent calcul: first-order logic
   108 				modal logics T, S4, S43
   109 				intuitionistic linear logic
   110   CCL		Martin Coen's Classical Computational Logic
   111   Cube		Barendregt's Lambda Cube
   112 
   113 David Aspinall has written a user interface for Isabelle.  It runs under
   114 GNU Emacs.  It's useful to both novices and experts.  You can get it by ftp
   115 from ftp.dcs.ed.ac.uk, file /pub/da/Isamode.tar.gz.
   116 
   117 Object-logics include examples files in subdirectory ex or file ex.ML.
   118 These files can be loaded in batch mode.  The commands can also be
   119 executed interactively, using the windows on your workstation.  This is a
   120 good way to get started.
   121 
   122 Each object-logic is built on top of Pure Isabelle, and possibly on top of
   123 another object logic like FOL or HOL.  A database or binary called Pure is
   124 first created, then the object-logic is loaded on top.  Poly/ML extends
   125 Pure using its "make_database" operation.  Standard ML of New Jersey starts
   126 with the Pure core image and loads the object-logic's ROOT.ML.
   127 
   128 ------------------------------------------------------------------------------
   129 
   130 The electronic mailing list isabelle-users@cl.cam.ac.uk provides a forum
   131 for Isabelle users to discuss problems and exchange information.  To join,
   132 send a message to isabelle-users-request@cl.cam.ac.uk.
   133 
   134 ------------------------------------------------------------------------------
   135 
   136 Please report any problems you encounter.  While we shall try to be helpful,
   137 we can accept no responsibility for the deficiences of Isabelle and their
   138 consequences.
   139 
   140 Lawrence C Paulson		E-mail: lcp@cl.cam.ac.uk
   141 Computer Laboratory 		Phone: +44-223-334600
   142 University of Cambridge 	Fax:   +44-223-334748 
   143 Pembroke Street 
   144 Cambridge CB2 3QG 
   145 England
   146 
   147 Tobias Nipkow			E-mail: nipkow@informatik.tu-muenchen.de
   148 Institut für Informatik		Phone: +49-89-2105-2690
   149 T. U. München			Fax:   +49-89-2105-8183
   150 D-80290 München
   151 Germany
   152 
   153 $Id$