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: clasohm@0: THE MAKEFILES clasohm@0: clasohm@0: The Makefiles can use two different Standard ML compilers: Poly/ML version lcp@86: 2.03 or later (from Abstract Hardware Ltd) and Standard ML of New Jersey lcp@86: (Version 0.93 or later). Poly/ML is a commercial product and costs money, clasohm@0: but it is reliable and its database system is convenient for interactive lcp@196: work. SML of New Jersey requires lots of store and disc space, but it is clasohm@0: free and its code sometimes runs faster. Both compilers are perfectly clasohm@0: satisfactory for running Isabelle. 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@2119: ISABELLECOMP is the ML compiler, typically "poly -noDisplay" or "/bin/sml". 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: lcp@86: If a Poly/ML session fails with the message "Run out of store" then you lcp@86: have used up the entire heap. If your tactic is not in a loop, allocating lcp@86: more heap at startup should correct the problem. For instance, "poly -h lcp@86: 15000" allocates sufficient heap space to rebuild all Isabelle examples. clasohm@0: 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: lcp@86: FOL Natural deduction First-Order Logic (intuitionistic and classical) lcp@86: FOLP First-Order Logic with Proof terms lcp@86: ZF Zermelo-Fraenkel set theory lcp@370: HOL Classical Higher-Order Logic lcp@370: LCF Logic for Computable Functions (domain theory) built upon FOL lcp@370: HOLCF A version of LCF built upon HOL lcp@86: CTT Constructive Type Theory lcp@86: LK Classical first-order sequent calculus lcp@86: Modal The modal logics T, S4, S43 lcp@86: CCL Martin Coen's Classical Computational Logic lcp@86: 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 lcp@196: another object logic like FOL or LK. 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: HOW TO GET A STANDARD ML COMPILER clasohm@0: clasohm@0: To obtain Poly/ML, contact Mike Crawley at Abstract clasohm@0: Hardware Ltd, The Howell Building, Brunel University, Uxbridge UB8 3PH, clasohm@0: England. clasohm@0: clasohm@0: To obtain Standard ML of New Jersey, contact David MacQueen clasohm@0: at AT&T Bell Laboratories, 600 Mountain Avenue, clasohm@0: Murray Hill, NJ 07974, USA. This compiler is available by FTP. Connect to clasohm@0: research.att.com; login as anonymous with your userid as password; set clasohm@0: binary mode; transfer files from the directory dist/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$