From 740a5c7544a68ba5d5d569fb591e38452f3105e8 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Sun, 31 Jan 2021 22:36:45 +0100 Subject: update magical documentation in manual for vok feature --- doc/ProofGeneral.texi | 26 ++++++++++++++++++-------- 1 file changed, 18 insertions(+), 8 deletions(-) (limited to 'doc') diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 22d4e6d6..d3ca8f9e 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -4960,19 +4960,29 @@ is not adapted. @c TEXI DOCSTRING MAGIC: coq-max-background-second-stage-percentage -@defvar coq-max-background-vio2vo-percentage -Percentage of @samp{@code{coq-max-background-vio2vo-percentage}} for vio2vo jobs.@* -This setting configures the maximal number of vio2vo background -jobs (if you set @samp{@code{coq-compile-quick}} to @code{'quick-and-vio2vo}) as +@defvar coq-max-background-second-stage-percentage +Percentage of @samp{@code{coq-max-background-compilation-jobs}} for the second stage.@* +This setting configures the maximal number of @samp{`-vok}' or vio2vo background +jobs running in a second stage as percentage of @samp{@code{coq-max-background-compilation-jobs}}. + +For backward compatibility, if this option is not customized, it +is initialized from the now deprecated option +@samp{@code{coq-max-background-vio2vo-percentage}}. @end defvar @c TEXI DOCSTRING MAGIC: coq-compile-second-stage-delay -@defvar coq-compile-vio2vo-delay -Delay in seconds for the vio2vo compilation.@* -This delay helps to avoid running into a library inconsistency -with @code{'quick-and-vio2vo}, see Coq issue #@var{5223}. +@defvar coq-compile-second-stage-delay +Delay in seconds before starting the second stage compilation.@* +The delay is applied to both @samp{`-vok}' and vio2vo second stages. +For Coq < 8.11 and vio2vo delay helps to avoid running into a +library inconsistency with @code{'quick-and-vio2vo}, see Coq issue +#@var{5223}. + +For backward compatibility, if this option is not customized, it +is initialized from the now deprecated option +@samp{@code{coq-compile-vio2vo-delay}}. @end defvar Locking ancestors can be disabled with the following option. -- cgit v1.2.3