Instructions for installing Proof General ========================================= This file describes what to do to run Proof General. Please let us know if you have problems trying to install it. Unpack this distribution somewhere. It will create a top-level directory containing Proof General, called Proof-General-. Put this line in your emacs file: (load-file "/generic/proof-site.el") Where is replaced by the full path name for Proof-General-. The command above will set the Emacs load path and add auto-loads for the assistants below: .v Coq files .l LEGO files .thy,.ML Isabelle files When you load a file with one of these extensions, the corresponding Proof General mode will be entered. In case of difficulty, please check the documentation in doc/, the notes below, and the file BUGS. If this doesn't help, then contact us via the address below. Proof General maintainer School of Computer Science, Division Of Informatics, University of Edinburgh. Edinburgh. http://www.dcs.ed.ac.uk/home/proofgen ---------------------------------------------------------------------- Notes for Proof General ======================= Byte Compilation. ----------------- Compilation of the Emacs lisp files improves efficiency but can sometimes cause compatibility problems. You can compile Proof General by typing 'make' in the directory where you installed it. Site-wide Installation ---------------------- If you are installing Proof General site-wide, you can put the components in the standard directories of the filesystem if you prefer, providing the variables in proof-site.el are adjusted accordingly. Make sure that the generic and assistant-specific elisp files are kept in subdirectories of proof-home so that the autoload directory calculations are correct. Removing support for unwanted provers ------------------------------------- You cannot run more than one instance of Proof General at a time: e.g. if you're using Coq, don't edit .ML files! If there are some assistants supported that you never want to use, you can remove them from the variable `proof-assistants` in proof-site.el to prevent an error message when you try to edit two different kinds of script file. The easiest way to do this (and other customization of Proof General) is via the Customize mechanism, see the menu: Options -> Customize -> Emacs -> External -> Proof General or, after loading Proof General, in a proof script buffer Proof-General -> Customize You may need extra customization depending on the proof assistant (for example, the name of the proof assistant binary). See the menu Proof-General -> Customize -> and the notes below for more details. Notice that the customization mechanism is only available in Emacs 20.x and XEmacs. ---------------------------------------------------------------------- Notes for Coq ============= If you want to use this mode for Coq, you need to make sure you have an appropriate version, which is from later than 1 March 1998. Check the values of coq-tags and coq-prog-name in coq.el to see that they correspond to the paths for coqtop and the library on your system. Install coqtags in a standard place or add /coq to your PATH. NB: You may need to change the path to perl at the top of the file. If you are running Coq, generate a TAGS file for the library by running coqtags `find . -name \*.v -print` in the root directory of the library, $COQTOP/theories. If you are running LEGO, do the same using legotags in the appropriate directory. ---------------------------------------------------------------------- Notes for LEGO ============== Install legotags in a standard place or add /lego to your PATH. NB: You may need to change the path to perl at the top of the file. ---------------------------------------------------------------------- Notes for Isabelle ================== Check the value of isabelle-prog-name. The distribution includes a version of Isamode's theory file mode. Use C-h m to check on the features available. Proof General attempts to lock theory files as well as ML files when they are loaded. It also attempts to load the theory file for a .ML file automatically before you start scripting. This is tricky because Isabelle's theory loader assumes that ML files are always read together with theory files. At the moment Proof General uses an altered version of use_thy which doesn't load the top-level ML file. This can cause confusion in the theory loader later, especially with update(). To be safe, try to use just the Proof General interface, and report any problems to isabelle@dcs.ed.ac.uk.