From dd10128c6cd822c1a16109bffc5b4fb67dc3ce49 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 29 Mar 2018 17:18:52 +0200 Subject: [Sphinx] Move chapter 28 to new infrastructure --- doc/refman/AsyncProofs.tex | 221 ---------------------- doc/refman/Reference-Manual.tex | 1 - doc/sphinx/addendum/parallel-proof-processing.rst | 221 ++++++++++++++++++++++ 3 files changed, 221 insertions(+), 222 deletions(-) delete mode 100644 doc/refman/AsyncProofs.tex create mode 100644 doc/sphinx/addendum/parallel-proof-processing.rst (limited to 'doc') diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex deleted file mode 100644 index 8f9d876cb..000000000 --- a/doc/refman/AsyncProofs.tex +++ /dev/null @@ -1,221 +0,0 @@ -\achapter{Asynchronous and Parallel Proof Processing\label{Asyncprocessing}} -%HEVEA\cutname{async-proofs.html} -\aauthor{Enrico Tassi} - -\label{pralitp} -\index{Asynchronous and Parallel Proof Processing!presentation} - -This chapter explains how proofs can be asynchronously processed by Coq. -This feature improves the reactivity of the system when used in interactive -mode via CoqIDE. In addition, it allows Coq to take advantage of -parallel hardware when used as a batch compiler by decoupling the checking -of statements and definitions from the construction and checking of proofs -objects. - -This feature is designed to help dealing with huge libraries of theorems -characterized by long proofs. In the current state, it may not be beneficial -on small sets of short files. - -This feature has some technical limitations that may make it unsuitable for -some use cases. - -For example, in interactive mode, some errors coming from the kernel of Coq -are signaled late. The type of errors belonging to this category -are universe inconsistencies. - -At the time of writing, only opaque proofs (ending with \texttt{Qed} or \texttt{Admitted}) can be processed asynchronously. - -Finally, asynchronous processing is disabled when running CoqIDE in Windows. The -current implementation of the feature is not stable on Windows. It can be -enabled, as described below at \ref{interactivecaveats}, though doing so is not -recommended. - -\section{Proof annotations} - -To process a proof asynchronously Coq needs to know the precise statement -of the theorem without looking at the proof. This requires some annotations -if the theorem is proved inside a \texttt{Section} (see Section~\ref{Section}). - -When a section ends, Coq looks at the proof object to decide which -section variables are actually used and hence have to be quantified in the -statement of the theorem. To avoid making the construction of proofs -mandatory when ending a section, one can start each proof with the -\texttt{Proof using} command (Section~\ref{ProofUsing}) that declares which -section variables the theorem uses. - -The presence of \texttt{Proof using} is needed to process proofs -asynchronously in interactive mode. - -It is not strictly mandatory in batch mode if it is not the first time -the file is compiled and if the file itself did not change. When the -proof does not begin with \texttt{Proof using}, the system records in an -auxiliary file, produced along with the \texttt{.vo} file, the list of -section variables used. - -\subsubsection{Automatic suggestion of proof annotations} - -The command \texttt{Set Suggest Proof Using} makes Coq suggest, when a -\texttt{Qed} command is processed, a correct proof annotation. It is up -to the user to modify the proof script accordingly. - -\section{Proof blocks and error resilience} - -Coq 8.6 introduces a mechanism for error resiliency: in interactive mode Coq -is able to completely check a document containing errors instead of bailing -out at the first failure. - -Two kind of errors are supported: errors occurring in vernacular commands and -errors occurring in proofs. - -To properly recover from a failing tactic, Coq needs to recognize the structure of -the proof in order to confine the error to a sub proof. Proof block detection -is performed by looking at the syntax of the proof script (i.e. also looking at indentation). -Coq comes with four kind of proof blocks, and an ML API to add new ones. - -\begin{description} -\item[curly] blocks are delimited by \texttt{\{} and \texttt{\}}, see \ref{Proof-handling} -\item[par] blocks are atomic, i.e. just one tactic introduced by the \texttt{par:} goal selector -\item[indent] blocks end with a tactic indented less than the previous one -\item[bullet] blocks are delimited by two equal bullet signs at the same indentation level -\end{description} - -\subsection{Caveats} - -When a vernacular command fails the subsequent error messages may be bogus, i.e. caused by -the first error. Error resiliency for vernacular commands can be switched off passing -\texttt{-async-proofs-command-error-resilience off} to CoqIDE. - -An incorrect proof block detection can result into an incorrect error recovery and -hence in bogus errors. Proof block detection cannot be precise for bullets or -any other non well parenthesized proof structure. Error resiliency can be -turned off or selectively activated for any set of block kind passing to -CoqIDE one of the following options: -\texttt{-async-proofs-tactic-error-resilience off}, -\texttt{-async-proofs-tactic-error-resilience all}, -\texttt{-async-proofs-tactic-error-resilience $blocktype_1$,..., $blocktype_n$}. -Valid proof block types are: ``curly'', ``par'', ``indent'', ``bullet''. - -\section{Interactive mode} - -At the time of writing the only user interface supporting asynchronous proof -processing is CoqIDE. - -When CoqIDE is started, two Coq processes are created. The master one follows -the user, giving feedback as soon as possible by skipping proofs, which are -delegated to the worker process. The worker process, whose state can be seen -by clicking on the button in the lower right corner of the main CoqIDE window, -asynchronously processes the proofs. If a proof contains an error, it is -reported in red in the label of the very same button, that can also be used to -see the list of errors and jump to the corresponding line. - -If a proof is processed asynchronously the corresponding \texttt{Qed} command -is colored using a lighter color that usual. This signals that -the proof has been delegated to a worker process (or will be processed -lazily if the \texttt{-async-proofs lazy} option is used). Once finished, the -worker process will provide the proof object, but this will not be -automatically checked by the kernel of the main process. To force -the kernel to check all the proof objects, one has to click the button -with the gears. Only then are all the universe constraints checked. - -\subsubsection{Caveats} -\label{interactivecaveats} - -The number of worker processes can be increased by passing CoqIDE the -\texttt{-async-proofs-j $n$} flag. Note that the memory consumption -increases too, since each worker requires the same amount of memory as -the master process. Also note that increasing the number of workers may -reduce the reactivity of the master process to user commands. - -To disable this feature, one can pass the \texttt{-async-proofs off} flag to -CoqIDE. Conversely, on Windows, where the feature is disabled by default, -pass the \texttt{-async-proofs on} flag to enable it. - -Proofs that are known to take little time to process are not delegated to a -worker process. The threshold can be configure with \texttt{-async-proofs-delegation-threshold}. Default is 0.03 seconds. - -\section{Batch mode} - -When Coq is used as a batch compiler by running \texttt{coqc} or -\texttt{coqtop -compile}, it produces a \texttt{.vo} file for each -\texttt{.v} file. A \texttt{.vo} file contains, among other things, -theorems statements and proofs. Hence to produce a \texttt{.vo} Coq need -to process all the proofs of the \texttt{.v} file. - -The asynchronous processing of proofs can decouple the generation of a -compiled file (like the \texttt{.vo} one) that can be loaded by -\texttt{Require} from the generation and checking of the proof objects. -The \texttt{-quick} flag can be passed to \texttt{coqc} or -\texttt{coqtop} to produce, quickly, \texttt{.vio} files. Alternatively, -when using a \texttt{Makefile} produced by \texttt{coq\_makefile}, the -\texttt{quick} target can be used to compile all files using the -\texttt{-quick} flag. - -A \texttt{.vio} file can be loaded using \texttt{Require} exactly as a -\texttt{.vo} file but proofs will not be available (the \texttt{Print} -command produces an error). Moreover, some universe constraints might be -missing, so universes inconsistencies might go unnoticed. A -\texttt{.vio} file does not contain proof objects, but proof tasks, -i.e. what a worker process can transform into a proof object. - -Compiling a set of files with the \texttt{-quick} flag allows one to work, -interactively, on any file without waiting for all the proofs to be checked. - -When working interactively, one can fully check all the \texttt{.v} files by -running \texttt{coqc} as usual. - -Alternatively one can turn each \texttt{.vio} into the corresponding -\texttt{.vo}. All \texttt{.vio} files can be processed in parallel, -hence this alternative might be faster. The command \texttt{coqtop - -schedule-vio2vo 2 a b c} can be used to obtain a good scheduling for 2 -workers to produce \texttt{a.vo}, \texttt{b.vo}, and \texttt{c.vo}. When -using a \texttt{Makefile} produced by \texttt{coq\_makefile}, the -\texttt{vio2vo} target can be used for that purpose. Variable \texttt{J} -should be set to the number of workers, e.g. \texttt{make vio2vo J=2}. -The only caveat is that, while the \texttt{.vo} files obtained from -\texttt{.vio} files are complete (they contain all proof terms and -universe constraints), the satisfiability of all universe constraints has -not been checked globally (they are checked to be consistent for every -single proof). Constraints will be checked when these \texttt{.vo} files -are (recursively) loaded with \texttt{Require}. - -There is an extra, possibly even faster, alternative: just check the -proof tasks stored in \texttt{.vio} files without producing the -\texttt{.vo} files. This is possibly faster because all the proof tasks -are independent, hence one can further partition the job to be done -between workers. The \texttt{coqtop -schedule-vio-checking 6 a b c} -command can be used to obtain a good scheduling for 6 workers to check -all the proof tasks of \texttt{a.vio}, \texttt{b.vio}, and -\texttt{c.vio}. Auxiliary files are used to predict how long a proof task -will take, assuming it will take the same amount of time it took last -time. When using a \texttt{Makefile} produced by \texttt{coq\_makefile}, -the \texttt{checkproofs} target can be used to check all \texttt{.vio} -files. Variable \texttt{J} should be set to the number of workers, -e.g. \texttt{make checkproofs J=6}. As when converting \texttt{.vio} -files to \texttt{.vo} files, universe constraints are not checked to be -globally consistent. Hence this compilation mode is only useful for quick -regression testing and on developments not making heavy use of the $Type$ -hierarchy. - -\section{Limiting the number of parallel workers} -\label{coqworkmgr} - -Many Coq processes may run on the same computer, and each of them may start -many additional worker processes. -The \texttt{coqworkmgr} utility lets one limit the number of workers, globally. - -The utility accepts the \texttt{-j} argument to specify the maximum number of -workers (defaults to 2). \texttt{coqworkmgr} automatically starts in the -background and prints an environment variable assignment like -\texttt{COQWORKMGR\_SOCKET=localhost:45634}. The user must set this variable in -all the shells from which Coq processes will be started. If one uses just -one terminal running the bash shell, then \texttt{export `coqworkmgr -j 4`} will -do the job. - -After that, all Coq processes, e.g. \texttt{coqide} and \texttt{coqc}, -will honor the limit, globally. - - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index cfb3c625b..7e68dd752 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -117,7 +117,6 @@ Options A and B of the licence are {\em not} elected.} %END LATEX \part{Addendum to the Reference Manual} \include{AddRefMan-pre}% -\include{AsyncProofs}% Paral-ITP \include{Universes.v}% Universe polymorphes \include{Misc.v} %BEGIN LATEX diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst new file mode 100644 index 000000000..8f9d876cb --- /dev/null +++ b/doc/sphinx/addendum/parallel-proof-processing.rst @@ -0,0 +1,221 @@ +\achapter{Asynchronous and Parallel Proof Processing\label{Asyncprocessing}} +%HEVEA\cutname{async-proofs.html} +\aauthor{Enrico Tassi} + +\label{pralitp} +\index{Asynchronous and Parallel Proof Processing!presentation} + +This chapter explains how proofs can be asynchronously processed by Coq. +This feature improves the reactivity of the system when used in interactive +mode via CoqIDE. In addition, it allows Coq to take advantage of +parallel hardware when used as a batch compiler by decoupling the checking +of statements and definitions from the construction and checking of proofs +objects. + +This feature is designed to help dealing with huge libraries of theorems +characterized by long proofs. In the current state, it may not be beneficial +on small sets of short files. + +This feature has some technical limitations that may make it unsuitable for +some use cases. + +For example, in interactive mode, some errors coming from the kernel of Coq +are signaled late. The type of errors belonging to this category +are universe inconsistencies. + +At the time of writing, only opaque proofs (ending with \texttt{Qed} or \texttt{Admitted}) can be processed asynchronously. + +Finally, asynchronous processing is disabled when running CoqIDE in Windows. The +current implementation of the feature is not stable on Windows. It can be +enabled, as described below at \ref{interactivecaveats}, though doing so is not +recommended. + +\section{Proof annotations} + +To process a proof asynchronously Coq needs to know the precise statement +of the theorem without looking at the proof. This requires some annotations +if the theorem is proved inside a \texttt{Section} (see Section~\ref{Section}). + +When a section ends, Coq looks at the proof object to decide which +section variables are actually used and hence have to be quantified in the +statement of the theorem. To avoid making the construction of proofs +mandatory when ending a section, one can start each proof with the +\texttt{Proof using} command (Section~\ref{ProofUsing}) that declares which +section variables the theorem uses. + +The presence of \texttt{Proof using} is needed to process proofs +asynchronously in interactive mode. + +It is not strictly mandatory in batch mode if it is not the first time +the file is compiled and if the file itself did not change. When the +proof does not begin with \texttt{Proof using}, the system records in an +auxiliary file, produced along with the \texttt{.vo} file, the list of +section variables used. + +\subsubsection{Automatic suggestion of proof annotations} + +The command \texttt{Set Suggest Proof Using} makes Coq suggest, when a +\texttt{Qed} command is processed, a correct proof annotation. It is up +to the user to modify the proof script accordingly. + +\section{Proof blocks and error resilience} + +Coq 8.6 introduces a mechanism for error resiliency: in interactive mode Coq +is able to completely check a document containing errors instead of bailing +out at the first failure. + +Two kind of errors are supported: errors occurring in vernacular commands and +errors occurring in proofs. + +To properly recover from a failing tactic, Coq needs to recognize the structure of +the proof in order to confine the error to a sub proof. Proof block detection +is performed by looking at the syntax of the proof script (i.e. also looking at indentation). +Coq comes with four kind of proof blocks, and an ML API to add new ones. + +\begin{description} +\item[curly] blocks are delimited by \texttt{\{} and \texttt{\}}, see \ref{Proof-handling} +\item[par] blocks are atomic, i.e. just one tactic introduced by the \texttt{par:} goal selector +\item[indent] blocks end with a tactic indented less than the previous one +\item[bullet] blocks are delimited by two equal bullet signs at the same indentation level +\end{description} + +\subsection{Caveats} + +When a vernacular command fails the subsequent error messages may be bogus, i.e. caused by +the first error. Error resiliency for vernacular commands can be switched off passing +\texttt{-async-proofs-command-error-resilience off} to CoqIDE. + +An incorrect proof block detection can result into an incorrect error recovery and +hence in bogus errors. Proof block detection cannot be precise for bullets or +any other non well parenthesized proof structure. Error resiliency can be +turned off or selectively activated for any set of block kind passing to +CoqIDE one of the following options: +\texttt{-async-proofs-tactic-error-resilience off}, +\texttt{-async-proofs-tactic-error-resilience all}, +\texttt{-async-proofs-tactic-error-resilience $blocktype_1$,..., $blocktype_n$}. +Valid proof block types are: ``curly'', ``par'', ``indent'', ``bullet''. + +\section{Interactive mode} + +At the time of writing the only user interface supporting asynchronous proof +processing is CoqIDE. + +When CoqIDE is started, two Coq processes are created. The master one follows +the user, giving feedback as soon as possible by skipping proofs, which are +delegated to the worker process. The worker process, whose state can be seen +by clicking on the button in the lower right corner of the main CoqIDE window, +asynchronously processes the proofs. If a proof contains an error, it is +reported in red in the label of the very same button, that can also be used to +see the list of errors and jump to the corresponding line. + +If a proof is processed asynchronously the corresponding \texttt{Qed} command +is colored using a lighter color that usual. This signals that +the proof has been delegated to a worker process (or will be processed +lazily if the \texttt{-async-proofs lazy} option is used). Once finished, the +worker process will provide the proof object, but this will not be +automatically checked by the kernel of the main process. To force +the kernel to check all the proof objects, one has to click the button +with the gears. Only then are all the universe constraints checked. + +\subsubsection{Caveats} +\label{interactivecaveats} + +The number of worker processes can be increased by passing CoqIDE the +\texttt{-async-proofs-j $n$} flag. Note that the memory consumption +increases too, since each worker requires the same amount of memory as +the master process. Also note that increasing the number of workers may +reduce the reactivity of the master process to user commands. + +To disable this feature, one can pass the \texttt{-async-proofs off} flag to +CoqIDE. Conversely, on Windows, where the feature is disabled by default, +pass the \texttt{-async-proofs on} flag to enable it. + +Proofs that are known to take little time to process are not delegated to a +worker process. The threshold can be configure with \texttt{-async-proofs-delegation-threshold}. Default is 0.03 seconds. + +\section{Batch mode} + +When Coq is used as a batch compiler by running \texttt{coqc} or +\texttt{coqtop -compile}, it produces a \texttt{.vo} file for each +\texttt{.v} file. A \texttt{.vo} file contains, among other things, +theorems statements and proofs. Hence to produce a \texttt{.vo} Coq need +to process all the proofs of the \texttt{.v} file. + +The asynchronous processing of proofs can decouple the generation of a +compiled file (like the \texttt{.vo} one) that can be loaded by +\texttt{Require} from the generation and checking of the proof objects. +The \texttt{-quick} flag can be passed to \texttt{coqc} or +\texttt{coqtop} to produce, quickly, \texttt{.vio} files. Alternatively, +when using a \texttt{Makefile} produced by \texttt{coq\_makefile}, the +\texttt{quick} target can be used to compile all files using the +\texttt{-quick} flag. + +A \texttt{.vio} file can be loaded using \texttt{Require} exactly as a +\texttt{.vo} file but proofs will not be available (the \texttt{Print} +command produces an error). Moreover, some universe constraints might be +missing, so universes inconsistencies might go unnoticed. A +\texttt{.vio} file does not contain proof objects, but proof tasks, +i.e. what a worker process can transform into a proof object. + +Compiling a set of files with the \texttt{-quick} flag allows one to work, +interactively, on any file without waiting for all the proofs to be checked. + +When working interactively, one can fully check all the \texttt{.v} files by +running \texttt{coqc} as usual. + +Alternatively one can turn each \texttt{.vio} into the corresponding +\texttt{.vo}. All \texttt{.vio} files can be processed in parallel, +hence this alternative might be faster. The command \texttt{coqtop + -schedule-vio2vo 2 a b c} can be used to obtain a good scheduling for 2 +workers to produce \texttt{a.vo}, \texttt{b.vo}, and \texttt{c.vo}. When +using a \texttt{Makefile} produced by \texttt{coq\_makefile}, the +\texttt{vio2vo} target can be used for that purpose. Variable \texttt{J} +should be set to the number of workers, e.g. \texttt{make vio2vo J=2}. +The only caveat is that, while the \texttt{.vo} files obtained from +\texttt{.vio} files are complete (they contain all proof terms and +universe constraints), the satisfiability of all universe constraints has +not been checked globally (they are checked to be consistent for every +single proof). Constraints will be checked when these \texttt{.vo} files +are (recursively) loaded with \texttt{Require}. + +There is an extra, possibly even faster, alternative: just check the +proof tasks stored in \texttt{.vio} files without producing the +\texttt{.vo} files. This is possibly faster because all the proof tasks +are independent, hence one can further partition the job to be done +between workers. The \texttt{coqtop -schedule-vio-checking 6 a b c} +command can be used to obtain a good scheduling for 6 workers to check +all the proof tasks of \texttt{a.vio}, \texttt{b.vio}, and +\texttt{c.vio}. Auxiliary files are used to predict how long a proof task +will take, assuming it will take the same amount of time it took last +time. When using a \texttt{Makefile} produced by \texttt{coq\_makefile}, +the \texttt{checkproofs} target can be used to check all \texttt{.vio} +files. Variable \texttt{J} should be set to the number of workers, +e.g. \texttt{make checkproofs J=6}. As when converting \texttt{.vio} +files to \texttt{.vo} files, universe constraints are not checked to be +globally consistent. Hence this compilation mode is only useful for quick +regression testing and on developments not making heavy use of the $Type$ +hierarchy. + +\section{Limiting the number of parallel workers} +\label{coqworkmgr} + +Many Coq processes may run on the same computer, and each of them may start +many additional worker processes. +The \texttt{coqworkmgr} utility lets one limit the number of workers, globally. + +The utility accepts the \texttt{-j} argument to specify the maximum number of +workers (defaults to 2). \texttt{coqworkmgr} automatically starts in the +background and prints an environment variable assignment like +\texttt{COQWORKMGR\_SOCKET=localhost:45634}. The user must set this variable in +all the shells from which Coq processes will be started. If one uses just +one terminal running the bash shell, then \texttt{export `coqworkmgr -j 4`} will +do the job. + +After that, all Coq processes, e.g. \texttt{coqide} and \texttt{coqc}, +will honor the limit, globally. + + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "Reference-Manual" +%%% End: -- cgit v1.2.3