--- 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.
--- 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
--- 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)