From c45e36f4de1b803aac623cb819f39842e54837d6 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Wed, 21 Jun 2017 15:32:18 -0400
Subject: disable async on Windows by default

---
 doc/refman/AsyncProofs.tex | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

(limited to 'doc/refman/AsyncProofs.tex')

diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex
index 7ffe252253..b93ca29577 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.
-- 
cgit v1.2.3

