diff options
Diffstat (limited to 'doc/ProofGeneral.texi')
| -rw-r--r-- | doc/ProofGeneral.texi | 171 |
1 files changed, 83 insertions, 88 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index dfa09085..aca9d21e 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -1728,7 +1728,7 @@ Query the user and exit the proof process. This simply kills the @samp{@code{proof-shell-buffer}} relying on the hook function -@samp{@code{proof-shell-kill-function}} to do the hard work. If optional +@samp{@code{proof-shell-kill-function}} to do the hard work. If optional argument @var{dont-ask} is non-nil, the proof process is terminated without confirmation. @@ -2306,11 +2306,13 @@ The size of the ring is set by the variable @code{pg-input-ring-size}. @c TEXI DOCSTRING MAGIC: pg-previous-input @deffn Command pg-previous-input arg -Cycle backwards through input history, saving input. +Cycle backwards through input history, saving input.@* +If called interactively, @var{arg} is given by the prefix argument. @end deffn @c TEXI DOCSTRING MAGIC: pg-next-input @deffn Command pg-next-input arg -Cycle forwards through input history. +Cycle forwards through input history.@* +If called interactively, @var{arg} is given by the prefix argument. @end deffn @c TEXI DOCSTRING MAGIC: pg-previous-matching-input @deffn Command pg-previous-matching-input regexp n @@ -2685,7 +2687,7 @@ Show a buffer of all the shortcuts available. @deffn Command unicode-tokens-list-unicode-chars Insert each Unicode character into a buffer.@* Lets you see which characters are available for literal display -in your emacs font. +in your Emacs font. (fn) @end deffn @@ -3467,49 +3469,40 @@ For multiple frame mode, this function obeys the setting of For single frame mode: -@itemize @bullet -@item -In two panes mode, this uses a canonical layout made by splitting -Emacs windows in equal proportions. The splitting is vertical if -emacs width is smaller than @samp{@code{split-width-threshold}} and -horizontal otherwise. You can then adjust the proportions by +- In two panes mode, this uses a canonical layout made by splitting +Emacs windows in equal proportions. The splitting is vertical if +Emacs width is smaller than @samp{@code{split-width-threshold}} and +horizontal otherwise. You can then adjust the proportions by dragging the separating bars. -@item -In three pane mode, there are three display modes, depending -where the three useful buffers are displayed: scripting -buffer, goals buffer and response buffer. - -Here are the three modes: - -@itemize @bullet -@item -@code{vertical}: the 3 buffers are displayed in one column. - -@item -@code{hybrid}: 2 columns mode, left column displays scripting buffer -and right column displays the 2 others. - -@item -@code{horizontal}: 3 columns mode, one for each buffer (script, goals, response). -@end itemize - -By default, the display mode is automatically chosen by -considering the current emacs frame width: if it is smaller -than @samp{@code{split-width-threshold}} then vertical mode is chosen, -otherwise if it is smaller than 1.5 * @samp{@code{split-width-threshold}} -then hybrid mode is chosen, finally if the frame is larger than -1.5 * @samp{@code{split-width-threshold}} then the horizontal mode is chosen. - -You can change the value of @samp{@code{split-width-threshold}} at your -will. - -If you want to force one of the layouts, you can set variable -@samp{@code{proof-three-window-mode-policy}} to @code{'vertical}, @code{'horizontal} or -@code{'hybrid}. The default value is @code{'smart} which sets the automatic -behaviour described above. -@end itemize - +- In three pane mode, there are three display modes, depending +@lisp + where the three useful buffers are displayed: scripting + buffer, goals buffer and response buffer. + + Here are the three modes: + + - vertical: the 3 buffers are displayed in one column. + - hybrid: 2 columns mode, left column displays scripting buffer + and right column displays the 2 others. + - horizontal: 3 columns mode, one for each buffer (script, goals, + response). + + By default, the display mode is automatically chosen by + considering the current Emacs frame width: if it is smaller + than @samp{@code{split-width-threshold}} then vertical mode is chosen, + otherwise if it is smaller than 1.5 * @samp{@code{split-width-threshold}} + then hybrid mode is chosen, finally if the frame is larger than + 1.5 * @samp{@code{split-width-threshold}} then the horizontal mode is chosen. + + You can change the value of @samp{@code{split-width-threshold}} at your + will. + + If you want to force one of the layouts, you can set variable + @samp{@code{proof-three-window-mode-policy}} to @code{'vertical}, @code{'horizontal} or + @code{'hybrid}. The default value is @code{'smart} which sets the automatic + behaviour described above. +@end lisp @end deffn @c TEXI DOCSTRING MAGIC: proof-shrink-windows-tofit @@ -3537,7 +3530,7 @@ Hovers will be added when this option is non-nil. Prover outputs can be displayed when the mouse hovers over the region that produced it and output is available (see @samp{@code{proof-full-annotation}}). If output is not available, the type of the output region is displayed. -Changes of this option will not be reflected in already-processed +Changes of this option will not be reflected in already-processed regions of the script. The default value is @code{nil}. @@ -3762,8 +3755,8 @@ locked (coloured blue); a buffer is completely unprocessed when there is no locked region. For some proof assistants (such as Coq) fully processed buffers make -no sense. Setting this option to @code{'process} has then the same effect -as leaving it unset (nil). (This behaviour is controlled by +no sense. Setting this option to @code{'process} has then the same effect +as leaving it unset (nil). (This behaviour is controlled by @samp{@code{proof-no-fully-processed-buffer}}.) The default value is @code{nil}. @@ -4427,17 +4420,16 @@ Documentation of the user option @code{coq-project-filename}: @c TEXI DOCSTRING MAGIC: coq-project-filename @defvar coq-project-filename The name of coq project file.@* -The coq project file of a coq development (Cf Coq documentation -on "makefile generation") should contain the arguments given to +The coq project file of a coq development (cf. Coq documentation on +"makefile generation") should contain the arguments given to coq_makefile. In particular it contains the -I and -R -options (preferably one per line). If @samp{coq-use-coqproject} is -t (default) the content of this file will be used by Proof General -to infer the @samp{@code{coq-load-path}} and the @samp{@code{coq-prog-args}} variables -that set the coqtop invocation by Proof General. This is now the -recommended way of configuring the coqtop invocation. Local file -variables may still be used to override the coq project file's -configuration. .dir-locals.el files also work and override -project file settings. +options (preferably one per line). If @samp{coq-use-coqproject} is +t (default) the content of this file will be used by Proof General to +infer the @samp{@code{coq-load-path}} and the @samp{@code{coq-prog-args}} variables that set +the coqtop invocation by Proof General. This is now the recommended +way of configuring the coqtop invocation. Local file variables may +still be used to override the coq project file's configuration. +.dir-locals.el files also work and override project file settings. @end defvar @@ -4451,8 +4443,8 @@ down to ``Coq Use Project File''). @c TEXI DOCSTRING MAGIC: coq-use-project-file @defvar coq-use-project-file -If t, when opening a coq file read the dominating _CoqProject.@* -If t, when a coq file is opened, Proof General will look for a +If t, when opening a Coq file read the dominating _CoqProject.@* +If t, when a Coq file is opened, Proof General will look for a project file (see @samp{@code{coq-project-filename}}) somewhere in the current directory or its parent directories. If there is one, its contents are read and used to determine the arguments that @@ -4891,7 +4883,7 @@ Coq Auto Compile -> Coq Auto Compile}. @defvar coq-compile-before-require If non-nil, check dependencies of required modules and compile if necessary.@* If non-nil ProofGeneral intercepts "Require" commands and checks if the -required library module and its dependencies are up-to-date. If not, they +required library module and its dependencies are up-to-date. If not, they are compiled from the sources before the "Require" command is processed. This option can be set/reset via menu @@ -4904,7 +4896,7 @@ This option can be set/reset via menu Buffers to save before checking dependencies for compilation.@* There are two orthogonal choices: Firstly one can save all or only the coq buffers, where coq buffers means all buffers in coq mode except the current -buffer. Secondly, Emacs can ask about each such buffer or save all of them +buffer. Secondly, Emacs can ask about each such buffer or save all of them unconditionally. This makes four permitted values: @code{'ask-coq} to confirm saving all @@ -4924,12 +4916,12 @@ The following options configure parallel compilation. @defvar coq-compile-parallel-in-background Choose the internal compilation method.@* When Proof General compiles itself, you have the choice between -two implementations. If this setting is nil, then Proof General +two implementations. If this setting is nil, then Proof General uses the old implementation and compiles everything sequentially -with synchronous job. With this old method Proof General is -locked during compilation. If this setting is t, then the new +with synchronous job. With this old method Proof General is +locked during compilation. If this setting is t, then the new method is used and compilation jobs are dispatched in parallel in -the background. The maximal number of parallel compilation jobs +the background. The maximal number of parallel compilation jobs is set with @samp{@code{coq-max-background-compilation-jobs}}. This option can be set/reset via menu @@ -4959,9 +4951,9 @@ This option can be set/reset via menu @defvar coq-max-background-compilation-jobs Maximal number of parallel jobs, if parallel compilation is enabled.@* Use the number of available CPU cores if this is set to -@code{'all-cpus}. This variable is the user setting. The value that is -really used is @samp{@code{coq--internal-max-jobs}}. Use @samp{@code{coq-max-jobs-setter}} -or the customization system to change this variable. Otherwise +@code{'all-cpus}. This variable is the user setting. The value that is +really used is @samp{@code{coq--internal-max-jobs}}. Use @samp{@code{coq-max-jobs-setter}} +or the customization system to change this variable. Otherwise your change will have no effect, because @samp{@code{coq--internal-max-jobs}} is not adapted. @end defvar @@ -4989,7 +4981,7 @@ Locking ancestors can be disabled with the following option. @defvar coq-lock-ancestors If non-nil, lock ancestor module files.@* If external compilation is used (via @samp{@code{coq-compile-command}}) then -only the direct ancestors are locked. Otherwise all ancestors are +only the direct ancestors are locked. Otherwise all ancestors are locked when the "Require" command is processed. This option can be set via menu @@ -5005,13 +4997,13 @@ configure the compilation command in @code{coq-compile-command}. @c TEXI DOCSTRING MAGIC: coq-compile-command @defvar coq-compile-command -External compilation command. If empty ProofGeneral compiles itself.@* +External compilation command. If empty ProofGeneral compiles itself.@* If unset (the empty string) ProofGeneral computes the dependencies of -required modules with coqdep and compiles as necessary. This internal +required modules with coqdep and compiles as necessary. This internal dependency checking does currently not handle ML modules. If a non-empty string, the denoted command is called to do the -dependency checking and compilation. Before executing this +dependency checking and compilation. Before executing this command the following keys are substituted as follows: @lisp %p the (physical) directory containing the source of @@ -5050,12 +5042,12 @@ configure these things with the following options. @defvar coq-load-path Non-standard coq library load path.@* This list specifies the LoadPath extension for coqdep, coqc and -coqtop. Usually, the elements of this list are strings (for +coqtop. Usually, the elements of this list are strings (for "-I") or lists of two strings (for "-R" dir path and "-Q" dir path). The possible forms of elements of this list correspond to the 4 -forms of include options (@samp{-I} @samp{-Q} and @samp{-R}). An element can be +forms of include options (@samp{-I} @samp{-Q} and @samp{-R}). An element can be @lisp - A list of the form @samp{(}ocamlimport dir)', specifying (in 8.5) a directory to be added to ocaml path (@samp{-I}). @@ -5086,10 +5078,10 @@ not the same (-I is for coq path). @c TEXI DOCSTRING MAGIC: coq-load-path-include-current @defvar coq-load-path-include-current -If @samp{t} let coqdep search the current directory too.@* -Should be @samp{t} for normal users. If @samp{t} pass -Q dir "" to coqdep when -processing files in directory "dir" in addition to any entries -in @samp{@code{coq-load-path}}. +If t, let coqdep search the current directory too.@* +Should be t for normal users. If t, pass -Q dir "" to coqdep when +processing files in directory "dir" in addition to any entries in +@samp{@code{coq-load-path}}. This setting is only relevant with Coq < 8.5. @end defvar @@ -5105,12 +5097,12 @@ libraries. @defvar coq-compile-ignored-directories Directories in which ProofGeneral should not compile modules.@* List of regular expressions for directories in which ProofGeneral -should not compile modules. If a library file name matches one +should not compile modules. If a library file name matches one of the regular expressions in this list then ProofGeneral does neither compile this file nor check its dependencies for -compilation. It makes sense to include non-standard coq library +compilation. It makes sense to include non-standard coq library directories here if they are not changed and if they are so big -that dependency checking takes noticeable time. The regular +that dependency checking takes noticeable time. The regular expressions in here are always matched against the .vo file name, regardless whether @samp{`-quick}' would be used to compile the file or not. @@ -5737,18 +5729,21 @@ Here are some of the other user options specific to EasyCrypt. You can set these as usual with the customization mechanism. @c TEXI DOCSTRING MAGIC: easycrypt-prog-name -@defvar easycrypt-prog-name +@defopt easycrypt-prog-name Name of program to run EasyCrypt. -@end defvar + +The default value is @code{"easycrypt"}. +@end defopt @c TEXI DOCSTRING MAGIC: easycrypt-load-path -@defvar easycrypt-load-path -Non-standard EasyCrypt library load path. This list specifies the -include path for EasyCrypt. +@defvar easycrypt-load-path +Non-standard EasyCrypt library load path.@* +This list specifies the include path for EasyCrypt. The elements of +this list are strings. @end defvar @c TEXI DOCSTRING MAGIC: easycrypt-web-page -@defvar easycrypt-web-page +@defvar easycrypt-web-page URL of web page for EasyCrypt. @end defvar |