--- a/NEWS Fri Sep 25 15:40:35 2020 +0200
+++ b/NEWS Fri Sep 25 15:43:53 2020 +0200
@@ -16,6 +16,9 @@
*** Isabelle/jEdit Prover IDE ***
+* Auto nitpick is enabled by default: it is now reasonably fast due to
+Kodkod invocation within Isabelle/Scala.
+
* The jEdit status line includes widgets both for JVM and ML heap usage.
Ongoing ML ongoing garbage collection is shown as "ML cleanup".
@@ -50,7 +53,7 @@
* Nitpick/Kodkod may be invoked directly within the running
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: false).
+guarded by system option "kodkod_scala" (default: true).
* Session HOL-Examples contains notable examples for Isabelle/HOL
(former entries of HOL-Isar_Examples, HOL-ex etc.).
--- a/src/HOL/Tools/etc/options Fri Sep 25 15:40:35 2020 +0200
+++ b/src/HOL/Tools/etc/options Fri Sep 25 15:43:53 2020 +0200
@@ -8,7 +8,7 @@
public option auto_time_limit : real = 2.0
-- "time limit for automatically tried tools (seconds > 0)"
-public option auto_nitpick : bool = false
+public option auto_nitpick : bool = true
-- "run Nitpick automatically"
public option auto_sledgehammer : bool = false
@@ -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 = false
+public option kodkod_scala : bool = true
-- "invoke Nitpick/Kodkod via Isabelle/Scala (instead of external process)"
public option kodkod_max_threads : int = 0