diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1998-11-12 15:23:56 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1998-11-12 15:23:56 +0000 |
| commit | b99d5190fa2d8973044bdc16c25c8f606f5efb71 (patch) | |
| tree | be503d7a3a07cde694602e4009b7d7b728566a8f /INSTALL | |
| parent | c67b03c51248f10e693f2c5f112dbc21f7d01298 (diff) | |
Minor fixes/improvements
Diffstat (limited to 'INSTALL')
| -rw-r--r-- | INSTALL | 22 |
1 files changed, 11 insertions, 11 deletions
@@ -1,8 +1,8 @@ Instructions for installing Proof General ========================================= -This file describes what to do to be able to run Proof General. -Please let us know if you have any problems in trying to install it. +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-<something>. @@ -10,8 +10,8 @@ Put this line in your emacs file: (load-file "<proofgeneral-home>/generic/proof-site.el") -Where <proofgeneral-home> is replaced by the full path to the -top-level directory made when you unpacked the distribution. +Where <proofgeneral-home> is replaced by the full path name for +Proof-General-<something>. The command above will set the Emacs load path and add auto-loads for the assistants below: @@ -64,14 +64,14 @@ directory calculations are correct. Removing support for unwanted provers ------------------------------------- -You cannot run more than one instance of Proof General at a time: so -if you're using Coq, don't edit .ML files! If there are some +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 solve this -problem. +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 most other customization of Proof -General) is via the Customize mechanism, see the menu: +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 @@ -116,7 +116,7 @@ running LEGO, do the same using legotags in the appropriate directory. Notes for LEGO ============== -Install legotags in a standard place or add <proof-home>/lego +Install legotags in a standard place or add <proofgeneral-home>/lego to your PATH. NB: You may need to change the path to perl at the top of the file. |