diff options
author | Paul Steckler <steck@stecksoft.com> | 2017-06-21 15:32:18 -0400 |
---|---|---|
committer | Paul Steckler <steck@stecksoft.com> | 2017-06-26 10:57:19 -0400 |
commit | c45e36f4de1b803aac623cb819f39842e54837d6 (patch) | |
tree | 7e292c878e4175483ca35e38ff38e9db75182fcf /doc/refman | |
parent | 4fbb431c81116b04e9c34cd7c6ffbf5d5f204f5e (diff) |
disable async on Windows by default
Diffstat (limited to 'doc/refman')
-rw-r--r-- | doc/refman/AsyncProofs.tex | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex index 7ffe25225..b93ca2957 100644 --- a/doc/refman/AsyncProofs.tex +++ b/doc/refman/AsyncProofs.tex @@ -6,7 +6,7 @@ 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 to that, it allows Coq to take advantage of +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. @@ -22,7 +22,12 @@ 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. -Last, at the time of writing, only opaque proofs (ending with \texttt{Qed} or \texttt{Admitted}) can be processed asynchronously. +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} @@ -112,6 +117,7 @@ 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 @@ -120,7 +126,8 @@ 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. +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. |