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 to 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 LFCS, 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, you won't be able to run LEGO scripts. If there are some assistants supported that you never want to use, you can remove them from the variable `proof-assistants` to prevent Proof General autoloading for files with particular extensions. This may be useful if you want to use other modes for those files, for example, you may want sml-mode for .ML files or Verilog mode for .v files. 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.