Merge PR #823: Async off in Windows by default in CoqIDE

2 files changed, 18 insertions, 4 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.
diff --git a/ide/coq.ml b/ide/coq.ml
index 8ecdf9caa..0fe831ab3 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -366,7 +366,14 @@ let bind_self_as f =
 (** This launches a fresh handle from its command line arguments. *)
 let spawn_handle args respawner feedback_processor =
   let prog = coqtop_path () in
-  let args = Array.of_list ("--xml_format=Ppcmds" :: "-async-proofs" :: "on" :: "-ideslave" :: args) in
+  let async_default =
+    (* disable async processing by default in Windows *)
+    if List.mem Sys.os_type ["Win32"; "Cygwin"] then
+      "off"
+    else
+      "on"
+  in
+  let args = Array.of_list ("--xml_format=Ppcmds" :: "-async-proofs" :: async_default :: "-ideslave" :: args) in
   let env =
     match !Flags.ideslave_coqtop_flags with
     | None -> None