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