# HG changeset patch
# User wenzelm
# Date 1488150028 -3600
# Node ID 002b4c8c366ebbb75db83b7890560c7a77c263b3
# Parent  12189e86c49d20737a96e0372d267af8fb229459
clarified defaults;

diff -r 12189e86c49d -r 002b4c8c366e NEWS
--- a/NEWS	Sun Feb 26 23:50:19 2017 +0100
+++ b/NEWS	Mon Feb 27 00:00:28 2017 +0100
@@ -123,6 +123,11 @@
 
 *** System ***
 
+* Option parallel_proofs is 1 by default (instead of more aggressive 2).
+This requires less heap space and avoids burning parallel CPU cycles,
+while full subproof parallelization is enabled for repeated builds
+(according to parallel_subproofs_threshold).
+
 * Prover IDE support for the Visual Studio Code editor and language
 server protocol, via the "isabelle vscode_server" tool (see also
 src/Tools/VSCode/README.md). The example application within the VS code
diff -r 12189e86c49d -r 002b4c8c366e etc/options
--- a/etc/options	Sun Feb 26 23:50:19 2017 +0100
+++ b/etc/options	Mon Feb 27 00:00:28 2017 +0100
@@ -71,7 +71,7 @@
 
 public option parallel_print : bool = true
   -- "parallel and asynchronous printing of results"
-public option parallel_proofs : int = 2
+public option parallel_proofs : int = 1
   -- "level of parallel proof checking: 0, 1, 2"
 option parallel_subproofs_threshold : real = 0.01
   -- "lower bound of timing estimate for forked nested proofs (seconds)"
diff -r 12189e86c49d -r 002b4c8c366e src/Pure/Admin/ci_profile.scala
--- a/src/Pure/Admin/ci_profile.scala	Sun Feb 26 23:50:19 2017 +0100
+++ b/src/Pure/Admin/ci_profile.scala	Mon Feb 27 00:00:28 2017 +0100
@@ -92,7 +92,7 @@
 
     val options =
       with_documents(Options.init())
-        .int.update("parallel_proofs", 2)
+        .int.update("parallel_proofs", 1)
         .int.update("threads", threads)
 
     print_section("BUILD")