From GitHub =========== Download and install Proof General from GitHub: git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG make -C ~/.emacs.d/lisp/PG Then add the following to your .emacs: ;; Open .v files with Proof General's Coq mode (require 'proof-site "~/.emacs.d/lisp/PG/generic/proof-site") This should be enough. Instructions for previous releases are below. Short Instructions for installing Proof General (details below) =============================================================== Proof General runs on a variety of platforms and with a variety of Emacs versions; see COMPATIBILITY for further notes. To install, unpack the 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-. If you prefer not to edit .emacs, you can use the script in bin/proofgeneral to launch Emacs with Proof General loaded. The command above will set the Emacs load path and add auto-loads for proof assistants, for example, visiting a file ending in .v will start Coq Proof General, and a file ending in .thy will start Isabelle Proof General. See the manual for a full list of file extensions and proof assistants, and the note below for how to disable those you don't need. In case of difficulty, please check the documentation in doc/, the notes below, the README file for each prover, and the file BUGS. If none of these files help, then contact me via the address below. David Aspinall, LFCS, School Of Informatics, University of Edinburgh. Edinburgh. http://proofgeneral.inf.ed.ac.uk/trac Detailed installation Notes for Proof General ============================================= Supported Emacs Versions. ------------------------- Please see COMPATIBILITY. If you're not sure of your version of Emacs, inspect the variable `emacs-version' by doing: C-h C-v emacs-version RET Other *recent* versions of either Emacs may also work, but please do not send bug reports for any version of Emacs which is more than a year older than the most recent stable release of that Emacs, unless you are reasonably sure that the bug has something to do with Proof General rather than Emacs. Unfortunately, compatibility across different Emacs versions is very difficult to maintain as APIs change frequently and bugs come and go between Emacs releases. Byte Compilation. ----------------- Compilation of the Emacs lisp files improves efficiency but can sometimes cause compatibility problems. In particular, byte compiled files are generally not compatible between different Emacs versions. We distribute .elcs for GNU Emacs 23.1, so you will have to delete them and (optionally) recompile for GNU Emacs 22. Use 'make clean' to remove all .elc files. Use 'make compile' to recompile .elc files. Check that the Makefile sets EMACS to your Emacs executable, or run 'make EMACS=/path/to/your/emacs' Dependency on Other Emacs Packages ---------------------------------- Proof General relies on several other Emacs packages, which are probably already supplied with your version of Emacs. If not, you will need to find them. These are the packages that you need to use Proof General: ESSENTIAL: * cl * custom * font-lock OPTIONAL: * outline * imenu * speedbar Included scripts ---------------- There are some included scripts which have hardwired paths. To try to edit these automatically to point to the right place, run make scripts 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-directory' so that the autoload directory calculations are correct. To save every user needing the line in their .emacs file, you can put that into a site-wide file like default.el, or using an automatically loaded file stored under site-start.d, if your distribution provides that. The provided Makefile will install everything in default locations: make install Will copy elisp, compiled elisp, documentation, and the "proofgeneral" shell script into perhaps sensible places. Try with "-n" or examine the Makefile carefully before use. Removing support for unwanted provers ------------------------------------- You cannot run more than one instance of Proof General at a time in the same Emacs process: 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 manual for more details. -------------------------------------------------------------------------- $Id$