diff options
Diffstat (limited to 'INSTALL')
| -rw-r--r-- | INSTALL | 158 |
1 files changed, 158 insertions, 0 deletions
diff --git a/INSTALL b/INSTALL new file mode 100644 index 00000000..2d27dd5b --- /dev/null +++ b/INSTALL @@ -0,0 +1,158 @@ +Instructions for installing Proof General +========================================= + +Proof General runs on a variety of platforms and with a variety of +Emacs versions; see notes below for particular hints. Please send us +additional hints for alternative platforms/Emacsen not mentioned. + +To install, unpack the distribution somewhere. It will create a +top-level directory containing Proof General, called +Proof-General-<something>. Put this line in your .emacs file: + + (load-file "<proofgeneral-home>/generic/proof-site.el") + +Where <proofgeneral-home> is replaced by the full path name to +Proof-General-<something>. 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/Isar 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 us via the address below. + + Proof General maintainer <support@proofgeneral.org> + LFCS, + Division Of Informatics, + University of Edinburgh. + Edinburgh. + + http://www.proofgeneral.org + + + +---------------------------------------------------------------------- + +Detailed installation Notes for Proof General +============================================= + + +RPM package. +------------ + +If you have the RPM file, this is the line you should add to your +.emacs file: + + (load-file "/usr/share/emacs/ProofGeneral/generic/proof-site.el") + + + +Running on Windows +------------------ + +We recommend XEmacs compiled for Windows, see http://www.xemacs.org. +Some Isabelle users have reported better operation with cygwin XEmacs. + +Unpack the Proof General tar or zip file, and rename the folder to +"ProofGeneral" to remove the version number. Put a line like this: + + (load-file "c:\\ProofGeneral\\generic\\proof-site.el") + +into .emacs. You should put .emacs in value of HOME if you set that, +or else in directory you installled XEmacs in, e.g. +c:\Program Files\XEmacs\.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. XEmacs is sometimes unbundled, so you may +need to select packages (or package groups) specially. These are the +packages that you need to use Proof General: + + ESSENTIAL: + * cl-macs + * comint + * custom + * font-lock + + OPTIONAL: + * outline + * func-menu + * X Symbol + + + +Byte Compilation. +----------------- + +Compilation of the Emacs lisp files improves efficiency but can +sometimes cause compatibility problems. It is not properly supported +in this release, because testing for these compatibility problems +takes too much time. If you want to experiment nonetheless, you can +compile Proof General by typing 'make' in the directory where you +installed it. This will result in lots of warnings and error messages +most of which can be ignored. Some files cannot be properly +byte-compiled at the moment because they contain settings which depend +on run-time; these will be deleted by the Makefile. Use 'make clean' +to remove all .elc files in case of problems. Check the Makefile sets +EMACS to your Emacs executable. + + +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. Read the Emacs manual for +details. + + +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 -> <Name of Assistant> + +and the manual for more details. + + + +$Id$ |