diff options
| -rw-r--r-- | FAQ | 18 | ||||
| -rw-r--r-- | doc/ProofGeneral.texi | 25 |
2 files changed, 40 insertions, 3 deletions
@@ -8,6 +8,24 @@ Please also check the BUGS file. ----------------------------------------------------------------- +Q. I use ProofGeneral with custom installations of Coq, depending + on the project I am working on. How can I change coq-prog-name + accordingly? + +A. The recommended way to set coq-prog-name is to create a file + .dir-locals.el in the top-level folder of your Coq project (or + if applicable, in the sub-folder containing the Coq source files) + with content: + + ((coq-mode . ((coq-prog-name . ".../path/to/coqtop")))) + + Then restart Emacs + (or just run: M-x proof-shell-exit RET yes RET, M-x normal-mode RET + in the Coq buffer before restarting the Coq process) in order + to take this change into account. + +----------------------------------------------------------------- + Q. The prover process produces some useful output I'd like to keep a note of, how do I do that? diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index bd5e591f..7c62debd 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -4028,11 +4028,17 @@ when a file is loaded. File variables and their values are written as a list at the end of the file. -@emph{Remarque 1:} The examples in the following are for Coq but the +@emph{Remark 1:} The examples in the following are for Coq but the trick is applicable to other provers. -@emph{Remarque 2:} For Coq specifically there is a recommended other way -of configuring coq options: project files (@ref{Using the Coq project file}). +@emph{Remark 2:} For Coq specifically, there is a recommended other way +of configuring Coq options: +project files (@ref{Using the Coq project file}). +Actually, project files are intended to be included in the +distribution of a library (and included in its repository), so the Coq +options specified in project files are supposed to work for all users. +In contrast, user-defined options such as @code{coq-prog-name} should +preferably be specified in a directory-local-variables file (see below). For example, in Coq projects involving multiple directories, it is necessary to set the variable @code{coq-load-path} @@ -4098,6 +4104,19 @@ The value in this file must be an alist that maps mode names to alists, where these latter alists map variables to values. You can aso put arbitrary code in this file @inforef{Directory Variables, ,emacs}. +Regarding the configuration of the @code{coq-prog-name} variable, the +@code{.dir-locals.el} file should contain something like: + +@lisp +((coq-mode . ((coq-prog-name . ".../path/to/coqtop")))) +@end lisp + +@emph{Note:} if you add such content to the @code{.dir-locals.el} file +you should restart Emacs to take this change into account (or +just run @kbd{M-x proof-shell-exit RET yes RET} +and @kbd{M-x normal-mode RET} in the Coq buffer +before restarting the Coq process). + @node Using abbreviations |