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