# HG changeset patch # User wenzelm # Date 864143900 -7200 # Node ID 68c7a70daa1683cdf06df0eec81275138dbd829f # Parent 0b74b9d4439eeafadfaff0d475d5864ab5572941 IMPORTANT NOTE: This is the old README. diff -r 0b74b9d4439e -r 68c7a70daa16 README.old --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/README.old Tue May 20 17:58:20 1997 +0200 @@ -0,0 +1,164 @@ + +*************************************************************************** + +IMPORTANT NOTE: This is the old README. The installation procedure +described below basically still works for Isabelle94-8, but will be +phased out next time. + +*************************************************************************** + + + + ISABELLE-94 DISTRIBUTION DIRECTORY + +------------------------------------------------------------------------------ +ISABELLE-94 IS INCOMPATIBLE WITH EARLIER VERSIONS. PLEASE CONSULT THE +DOCUMENTATION. + +In particular, theory files are no longer forced into lower case, but must +be identical to the actual theory name. See the script +conv-theory-files.pl on directory Tools. +------------------------------------------------------------------------------ + +This directory contains the complete Isabelle system. To build and test +all the Isabelle object-logics, use the shell script make-all (on directory +Tools). Pure Isabelle and each of the object-logics can be built +separately using the Makefiles in the respective directories; read them for +more information. + + HOW TO BUILD ISABELLE + +Here are brief instructions. For more detail, read further. + +1. Create a directory to hold the Isabelle executable images. + Set the environment variable ISABELLEBIN to its full (absolute) pathname. + +2. Set the environment variable ISABELLECOMP to the command to execute your + Standard ML compiler. + +3. If using Poly/ML, set the environment variable ML_DBASE to the full + pathname of the empty Poly/ML database. + +4. Change your working directory to that containing this file. + +5a. To build ALL logics and run examples, type "make-all" and wait up to + 10 hours. Standard ML of New Jersey will require up to 200M + of disc space! Poly/ML will require about 25M. + +-OR- +5b. To build ALL logics but run no examples, type "make-all -notest". This + is much faster than 5a but needs just as much disc space. + +-OR- +5c. To build just one logic, such as HOL, change to directory HOL and type + "make" or "make test". This may trigger further Makes automatically. + + + SUITABLE ML COMPILERS + +You can use two different Standard ML compilers: Poly/ML version 2.03 or later +(from Abstract Hardware Ltd) and Standard ML of New Jersey (Version 0.93 or +later). Poly/ML is a commercial product and costs money, but it is stable and +efficient; moreover its database system is convenient for interactive work. +SML/NJ needs lots of store and disc space, but it is free. Some recent +versions of SML/NJ are significantly faster than 0.93, but beware of many +incompatibilities among them; you might be forced to edit the file +Pure/NJ1xx.ML. VERSIONS BETWEEN 109.16 AND 109.21 ARE VERY SLOW. + +To obtain Poly/ML, contact Abstract Hardware Ltd, The Howell Building, Brunel +University, Uxbridge UB8 3PH, England, email lambda@ahl.co.uk. + +To obtain Standard ML of New Jersey, see the Web page + http://cm.bell-labs.com/cm/cs/what/smlnj/software.html +or send email to sml-nj@research.bell-labs.com. + + + ENVIRONMENT VARIABLES + +The Makefiles and make-all use environment variables that you should set +according to your site configuration. See file Tools/make-all-nj for an +example using the Bourne shell, sh. + +ISABELLEBIN is the directory to hold Poly/ML databases or New Jersey ML +images. This directory *must* be different from the Isabelle source +directory. ISABELLEBIN must be an absolute pathname (one starting with "/"). + +ML_DBASE is an *absolute* pathname to the initial Poly/ML database. It is not +required for New Jersey ML. + +ISABELLECOMP is the command to run ML compiler, typically "/bin/sml" or "poly +-noDisplay -h 15000". (The -h switch to Poly specifies an initial heap +allocation, which you should consider increasing if a command fails with the +message "Run out of store".) Please DO NOT use a command such as +"sml @SMLdebug=/dev/null", since the pathname after "sml" will confuse the +Makefiles. + +If, after stripping a leading pathname, the compiler begins with the letters +"poly" then the Makefiles assume Poly/ML. If it begins with the letters "sml" +then they assume Standard ML of New Jersey. + + + STRUCTURE OF THIS DIRECTORY + +Important files include... + COPYRIGHT Copyright notice and Disclaimer of Warranty + Pure contains source files for Pure Isabelle (no object-logic) + Provers contains generic theorem provers: simplifier, etc. + Tools contains shell scripts and utilities + +The following subdirectories contain object-logics: + FOL natural deduction First-Order Logic + (intuitionistic and classical versions) + FOLP First-Order Logic with Proof terms + ZF Zermelo-Fraenkel set theory + HOL Classical Higher-Order Logic + LCF Logic for Computable Functions (domain theory) built upon FOL + HOLCF A version of LCF built upon HOL + CTT Constructive Type Theory + Sequents Sequent calcul: first-order logic + modal logics T, S4, S43 + intuitionistic linear logic + CCL Martin Coen's Classical Computational Logic + Cube Barendregt's Lambda Cube + +David Aspinall has written a user interface for Isabelle. It runs under +GNU Emacs. It's useful to both novices and experts. You can get it by ftp +from ftp.dcs.ed.ac.uk, file /pub/da/Isamode.tar.gz. + +Object-logics include examples files in subdirectory ex or file ex.ML. +These files can be loaded in batch mode. The commands can also be +executed interactively, using the windows on your workstation. This is a +good way to get started. + +Each object-logic is built on top of Pure Isabelle, and possibly on top of +another object logic like FOL or HOL. A database or binary called Pure is +first created, then the object-logic is loaded on top. Poly/ML extends +Pure using its "make_database" operation. Standard ML of New Jersey starts +with the Pure core image and loads the object-logic's ROOT.ML. + +------------------------------------------------------------------------------ + +The electronic mailing list isabelle-users@cl.cam.ac.uk provides a forum +for Isabelle users to discuss problems and exchange information. To join, +send a message to isabelle-users-request@cl.cam.ac.uk. + +------------------------------------------------------------------------------ + +Please report any problems you encounter. While we shall try to be helpful, +we can accept no responsibility for the deficiences of Isabelle and their +consequences. + +Lawrence C Paulson E-mail: lcp@cl.cam.ac.uk +Computer Laboratory Phone: +44-223-334600 +University of Cambridge Fax: +44-223-334748 +Pembroke Street +Cambridge CB2 3QG +England + +Tobias Nipkow E-mail: nipkow@informatik.tu-muenchen.de +Institut für Informatik Phone: +49-89-2105-2690 +T. U. München Fax: +49-89-2105-8183 +D-80290 München +Germany + +$Id$