diff options
| -rw-r--r-- | CHANGES | 6 | ||||
| -rw-r--r-- | coq/coq-compile-common.el | 10 | ||||
| -rw-r--r-- | doc/ProofGeneral.texi | 47 |
3 files changed, 53 insertions, 10 deletions
@@ -26,6 +26,12 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac option `coq-compile-quick' or the subsection "11.3.3 Quick compilation and .vio Files" in the Coq reference manual. +*** new option coq-compile-keep-going (in menu Coq -> Auto Compilation) + + Similar to ``make -k'', with this option enabled, background + compilation does not stop at the first error but rather + continues as far as possible. + *** bug fixes - avoid leaving partial files behind when compilation fails - 123: Parallel background compliation fails to execute some diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index 40e3a4d7..92614e7a 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -234,6 +234,9 @@ quick-and-vio2vo Same as `quick-no-vio2vo', but start vio2vo processes compilation while you are processing stuff far below the last require. vio2vo compilation is done on a subset of the available cores, see `coq-compile-vio2vo-percentage'. + When `coq-compile-keep-going' is set, vio2vo compilation + is scheduled for those files for which coqc compilation + was successful. Warning: This mode does only work when you process require commands in batches. Slowly single-stepping through require's @@ -265,8 +268,11 @@ ensure-vo Ensure that all library dependencies are present as .vo "Continue compilation after the first error as far as possible. Similar to ``make -k'', with this option enabled, the background compilation continues after the first error as far as possible. -With this option disabled, the background compilation is -immediately stopped after the first error.") +With this option disabled, background compilation is +immediately stopped after the first error. + +This option can be set/reset via menu +`Coq -> Auto Compilation -> Keep going'.") ;; define coq-compile-keep-going-toggle (proof-deftoggle coq-compile-keep-going) diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 748cf3ac..31594b9d 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -4494,8 +4494,12 @@ these points: @itemize @bullet @item -The option @code{coq-compile-before-require} must be -turned on (menu @code{Coq -> Auto Compilation -> Compile Before Require}). +Set the option @code{coq-compile-before-require} (menu @code{Coq +-> Auto Compilation -> Compile Before Require}) to enable +compilation before processing @code{Require} commands and set +@code{coq-compile-parallel-in-background} (menu @code{Coq +-> Auto Compilation -> Parallel background compilation}) for +parallel asynchronous compilation (recommended). @item Nonstandard load path elements @emph{must} be configured via a Coq project file (this is the recommended option), @@ -4505,7 +4509,10 @@ option @code{coq-load-path}. @code{-I} or @code{-R} options in @item Configure @code{coq-max-background-compilation-jobs} if you want to limit -the number of parallel background jobs. +the number of parallel background jobs and set +@code{coq-compile-keep-going} (menu @code{Coq -> Auto Compilation +-> Keep going}) to let compilation continue after the first +error. @end itemize @@ -4554,7 +4561,16 @@ controls how @code{-quick} and @code{.vio} files are used, @ref{Quick compilation and .vio Files}. This can also be configured in the menu @code{Coq -> Auto Compilation}. -When a @code{Require} command causes a compilation of some files +Similar to @code{make -k}, background compilation can be +configured to continue as far as possible after the first error, +see option @code{coq-compile-keep-going} (menu @code{Coq -> Auto +Compilation -> Keep going}). The keep-going option only applies +to errors from @code{coqdep} and @code{coqc}. For all other +errors (for instance when the translation from logical module +names to physical files fails or when starting @code{coqc} or +@code{coqdep} fails), the compilation is immediately aborted. + +When a @code{Require} command causes a compilation of some files, one may wish to save some buffers to disk beforehand. The option @code{coq-compile-auto-save} controls how and which files are saved. There are two orthogonal choices: One may wish to save all @@ -4723,12 +4739,14 @@ files, but don't compile prerequisites for which an up-to-date @item quick-and-vio2vo Same as @code{quick-no-vio2vo}, but start vio2vo processes for missing @code{.vo} files after a certain delay when library -complication for the current queue region has finished. With this +compilation for the current queue region has finished. With this mode you might see asynchronous errors from vio2vo compilation while you are processing stuff far below the last require. vio2vo compilation is done on a subset of the available cores controlled by option @code{coq-compile-vio2vo-percentage}, @ref{Customizing -Coq Multiple File Support}. +Coq Multiple File Support}. When @code{coq-compile-keep-going} is +set, vio2vo compilation is scheduled for those files for which +@code{coqc} compilation was successful. @emph{Warning}: This mode does only work when you process require commands in batches. Slowly single-stepping through require's @@ -4816,14 +4834,27 @@ The option @code{coq-compile-quick} is described in detail above, @ref{Quick compilation and .vio Files} +@c TEXI DOCSTRING MAGIC: coq-compile-keep-going +@defvar coq-compile-keep-going +Continue compilation after the first error as far as possible.@* +Similar to @samp{`make -k}', with this option enabled, the background +compilation continues after the first error as far as possible. +With this option disabled, background compilation is +immediately stopped after the first error. + +This option can be set/reset via menu +@samp{Coq -> Auto Compilation -> Keep going}. +@end defvar + + @c TEXI DOCSTRING MAGIC: coq-max-background-compilation-jobs @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}} +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}} +your change will have no effect, because @samp{@code{coq--internal-max-jobs}} is not adapted. @end defvar |