update changes and documentation for vok feature

1 files changed, 37 insertions, 41 deletions

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index aca9d21e..22d4e6d6 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -4593,9 +4593,9 @@ compilation has finished.
 and dependencies on ML Modules reported by @code{coqdep} are
 ignored.
 
-Proof General uses @code{coqdep} in order to translate the
-qualified identifiers in @code{Require} commands to coq library
-file names and to determine library dependencies. Because Proof
+Proof General uses @code{coqdep} to determine which libraries a
+@code{Require} command will load and which files must be
+up-to-date. Because Proof
 General cannot know whether files are updated outside of Emacs,
 it checks for every @code{Require} command the complete
 dependency tree and recompiles files as necessary.
@@ -4621,10 +4621,9 @@ and via menu entries in @code{Coq -> Auto Compilation},
 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
+Compilation -> Keep going}). The keep-going option applies
+to errors from @code{coqdep} and @code{coqc}. However, when
+starting @code{coqc} or
 @code{coqdep} fails), the compilation is immediately aborted.
 
 When a @code{Require} command causes a compilation of some files,
@@ -4675,14 +4674,6 @@ compilation jobs.
 Parallel asynchronous compilation supports both vos and quick/vio
 compilation, but exclusively, depending on the Coq version,
 @ref{Quick and inconsistent compilation}. 
-
-Actually, even with parallel asynchronous compilation, not everything runs
-asynchronously. To translate module identifiers from the Coq
-sources into file names, Proof General runs coqdep on an
-automatically generated, one-line file. These coqdep jobs run
-synchronously while the Require commands are parsed. The coqdep
-jobs on the real source files do run asynchronously in the
-background. 
 @end table
 
 
@@ -4743,16 +4734,21 @@ detection of Proof General or by the setting
 @code{coq-pinned-version}) required modules are either compiled
 to @code{.vo} or @code{.vos} files, depending on the setting
 @code{coq-compile-vos}, which can also be set on menu @code{Coq
--> Auto Compilation -> vos compilation}. There are three choices:
+-> Auto Compilation -> vos compilation}. There are four choices:
 
 @table @asis
-@item @code{use-vos}
-Compile with @code{-vos}. Noticeably faster, but proofs are
-skipped during compilation and some universe constraints might be
-missing.
+@item @code{vos-and-vok}
+First compile using @code{-vos}, skipping proofs. When
+compilation finished, run @code{coqc -vok} in a second stage to
+check proofs on all files that require it. Some universe
+constraints might be missed, rendering this method possibly
+inconsistent.
+@item @code{vos}
+Only compile using @code{-vos}, skipping proofs. No @code{coqc
+-vok} run to check proofs. Obviously inconsistent.
 @item @code{ensure-vo}
 Compile without @code{-vos} to @code{.vo} files, checking all
-proofs and universe constraints.
+proofs and universe constraints. Only consistent choice.
 @item unset (@code{nil})
 Compile with @code{-vos} if @code{coq-compile-quick} (see below)
 equals @code{quick-no-vio2vo}. Otherwise compile without
@@ -4760,6 +4756,17 @@ equals @code{quick-no-vio2vo}. Otherwise compile without
 for users that configured @code{coq-compile-quick} in the past.
 @end table
 
+For @code{vos-and-vok} the second @code{-vok} stage runs
+asynchronously @code{coq-compile-second-stage-delay} seconds
+after the last @code{Require} command has been processed. Errors
+might pop up later and interrupt your normal interaction with
+Coq. Because the second stage is not time critical, it runs on
+@code{coq-max-background-second-stage-percentage} per cent of the
+cores configured for the first stage. When
+@code{coq-compile-keep-going} is configured and an error occurs,
+the second @code{-vok} stage is run on those dependencies not
+affected by the error.
+
 For Coq version 8.5 until before 8.11, Proof General supports
 quick or vio compilation with parallel asynchronous compilation.
 There are 4 modes that can be
@@ -4773,10 +4780,10 @@ that have not switched there development to
 @code{Proof using}. Use @code{quick-no-vio2vo}, if you want quick
 recompilation without producing .vo files. Option
 @code{quick-and-vio2vo} recompiles with @code{-quick}/@code{-vio} as
-@code{quick-no-vio2vo} does, but schedules a vio2vo compilation
-for missing @code{.vo} files after a certain delay. Finally, use
+@code{quick-no-vio2vo} does, but schedules a second vio2vo stage
+for missing @code{.vo} files. Finally, use
 @code{ensure-vo} for only importing @code{.vo} files with
-complete universe checks.
+complete universe checks. 
 
 Note that with all of @code{no-quick}, @code{quick-no-vio2vo} and
 @code{quick-and-vio2vo} your development might be unsound because
@@ -4833,16 +4840,9 @@ files, but don't compile prerequisites for which an up-to-date
 @code{.vo} file exists. Delete or overwrite outdated @code{.vio} files.
 
 @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
-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}. When @code{coq-compile-keep-going} is
-set, vio2vo compilation is scheduled for those files for which
-@code{coqc} compilation was successful.
+Same as @code{quick-no-vio2vo}, but start a second vio2vo stage for
+missing @code{.vo} files. Everything described previously for the
+second @code{-vok} stage applies here as well.
 
 @emph{Warning}: This mode does only work when you process require
 commands in batches. Slowly single-stepping through require's
@@ -4850,7 +4850,7 @@ might lead to inconsistency errors when loading some libraries,
 see Coq issue #5223. To mitigate this risk, vio2vo compilation
 only starts after a certain delay after the last require command
 of the current queue region has been processed. This is
-controlled by @code{coq-compile-vio2vo-delay}, @ref{Customizing
+controlled by @code{coq-compile-second-stage-delay}, @ref{Customizing
 Coq Multiple File Support}.
 
 @item ensure-vo
@@ -4959,7 +4959,7 @@ is not adapted.
 @end defvar
 
 
-@c TEXI DOCSTRING MAGIC: coq-max-background-vio2vo-percentage
+@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
@@ -4968,7 +4968,7 @@ percentage of @samp{@code{coq-max-background-compilation-jobs}}.
 @end defvar
 
 
-@c TEXI DOCSTRING MAGIC: coq-compile-vio2vo-delay
+@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
@@ -5117,10 +5117,6 @@ or not.
 No support for @code{Declare ML Module} commands and files
 depending on an ML module.
 @item
-Comments inside require commands should be avoided, see Proof
-General issue #352. The regular expression to extract module
-names does not skip over comments.
-@item
 When a compiled library has the same time stamp as the source
 file, it is considered outdated. Some old file systems (for
 instance ext3) or Emacs before version 24.3 support only time