# HG changeset patch
# User wenzelm
# Date 1637872310 -3600
# Node ID 91ee232b42115a65fe64c85cef37c3498aab2487
# Parent  90242c744a1a5e86696648a79e37d0860e5371c4
clarified default for kodkod_scala;
NEWS for proper release;

diff -r 90242c744a1a -r 91ee232b4211 NEWS
--- a/NEWS	Thu Nov 25 19:56:01 2021 +0100
+++ b/NEWS	Thu Nov 25 21:31:50 2021 +0100
@@ -208,6 +208,15 @@
 min.absorb4, max.absorb1, max.absorb2, max.absorb3, max.absorb4. Minor
 INCOMPATIBILITY.
 
+* Nitpick/Kodkod: default is back to external Java process (option
+kodkod_scala = false), both for PIDE and batch builds. This reduces
+confusion and increases robustness of timeouts, despite substantial
+overhead to run an external JVM. For more fine-grained control, the
+kodkod_scala option can be modified within the formal theory context
+like this:
+
+  declare [[kodkod_scala = false]]
+
 * Sledgehammer:
   - Update of bundled provers:
       . E 2.6
@@ -743,10 +752,7 @@
 Isabelle/Scala session (instead of an external Java process): this
 improves reactivity and saves resources. This experimental feature is
 guarded by system option "kodkod_scala" (default: true in PIDE
-interaction, false in batch builds) or configuration option within the
-theory context; it may be changed locally like this:
-
-  declare [[kodkod_scala = false]]
+interaction, false in batch builds).
 
 * Simproc "defined_all" and rewrite rule "subst_all" perform more
 aggressive substitution with variables from assumptions.
diff -r 90242c744a1a -r 91ee232b4211 src/HOL/Tools/etc/options
--- a/src/HOL/Tools/etc/options	Thu Nov 25 19:56:01 2021 +0100
+++ b/src/HOL/Tools/etc/options	Thu Nov 25 21:31:50 2021 +0100
@@ -38,7 +38,7 @@
 public option MaSh : string = "sml"
   -- "machine learning algorithm to use by Sledgehammer (nb_knn, nb, knn, none)"
 
-public option kodkod_scala : bool = true
+public option kodkod_scala : bool = false
   -- "invoke Nitpick/Kodkod via Isabelle/Scala (instead of external process)"
 
 public option kodkod_max_threads : int = 0
diff -r 90242c744a1a -r 91ee232b4211 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Nov 25 19:56:01 2021 +0100
+++ b/src/Pure/Tools/build.scala	Thu Nov 25 21:31:50 2021 +0100
@@ -191,7 +191,6 @@
       options +
         "completion_limit=0" +
         "editor_tracing_messages=0" +
-        "kodkod_scala=false" +
         ("pide_reports=" + options.bool("build_pide_reports"))
 
     val store = Sessions.store(build_options)