--- a/NEWS Thu Nov 25 12:54:21 2021 +0100
+++ b/NEWS Thu Nov 25 19:56:01 2021 +0100
@@ -743,7 +743,10 @@
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).
+interaction, false in batch builds) or configuration option within the
+theory context; it may be changed locally like this:
+
+ declare [[kodkod_scala = false]]
* Simproc "defined_all" and rewrite rule "subst_all" perform more
aggressive substitution with variables from assumptions.
--- a/src/HOL/Nitpick_Examples/Tests_Nits.thy Thu Nov 25 12:54:21 2021 +0100
+++ b/src/HOL/Nitpick_Examples/Tests_Nits.thy Thu Nov 25 19:56:01 2021 +0100
@@ -11,6 +11,6 @@
imports Main
begin
-ML \<open>() |> getenv "KODKODI" <> "" ? Nitpick_Tests.run_all_tests\<close>
+ML \<open>if getenv "KODKODI" = "" then () else Nitpick_Tests.run_all_tests \<^context>\<close>
end
--- a/src/HOL/Nitpick_Examples/minipick.ML Thu Nov 25 12:54:21 2021 +0100
+++ b/src/HOL/Nitpick_Examples/minipick.ML Thu Nov 25 19:56:01 2021 +0100
@@ -395,11 +395,12 @@
fun solve_any_kodkod_problem thy problems =
let
val {debug, overlord, timeout, ...} = Nitpick_Commands.default_params thy []
+ val kodkod_scala = Config.get_global thy Kodkod.kodkod_scala
val deadline = Timeout.end_time timeout
val max_threads = 1
val max_solutions = 1
in
- case solve_any_problem debug overlord deadline max_threads max_solutions
+ case solve_any_problem kodkod_scala debug overlord deadline max_threads max_solutions
problems of
Normal ([], _, _) => "none"
| Normal _ => "genuine"
--- a/src/HOL/Tools/Nitpick/kodkod.ML Thu Nov 25 12:54:21 2021 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Thu Nov 25 19:56:01 2021 +0100
@@ -166,7 +166,8 @@
val is_problem_trivially_false : problem -> bool
val problems_equivalent : problem * problem -> bool
val solve_any_problem :
- bool -> bool -> Time.time -> int -> int -> problem list -> outcome
+ bool -> bool -> bool -> Time.time -> int -> int -> problem list -> outcome
+ val kodkod_scala : bool Config.T
end;
structure Kodkod : KODKOD =
@@ -958,7 +959,7 @@
is partly due to the JVM and partly due to the ML "bash" function. *)
val fudge_ms = 250
-fun uncached_solve_any_problem overlord deadline max_threads0 max_solutions problems =
+fun uncached_solve_any_problem kodkod_scala overlord deadline max_threads0 max_solutions problems =
let
val j = find_index (curry (op =) True o #formula) problems
val indexed_problems = if j >= 0 then
@@ -975,8 +976,7 @@
then Options.default_int \<^system_option>\<open>kodkod_max_threads\<close>
else max_threads0
- val external_process =
- not (Options.default_bool \<^system_option>\<open>kodkod_scala\<close>) orelse overlord
+ val external_process = not kodkod_scala orelse overlord
val timeout0 = Time.toMilliseconds (deadline - Time.now ())
val timeout = if external_process then timeout0 - fudge_ms else timeout0
@@ -1058,11 +1058,11 @@
Synchronized.var "Kodkod.cached_outcome"
(NONE : ((int * problem list) * outcome) option)
-fun solve_any_problem debug overlord deadline max_threads max_solutions
+fun solve_any_problem kodkod_scala debug overlord deadline max_threads max_solutions
problems =
let
fun do_solve () =
- uncached_solve_any_problem overlord deadline max_threads max_solutions
+ uncached_solve_any_problem kodkod_scala overlord deadline max_threads max_solutions
problems
in
if debug orelse overlord then
@@ -1085,4 +1085,6 @@
end
end
+val kodkod_scala = Attrib.setup_option_bool (\<^system_option>\<open>kodkod_scala\<close>, \<^here>)
+
end;
--- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Nov 25 12:54:21 2021 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Nov 25 19:56:01 2021 +0100
@@ -692,6 +692,7 @@
fun solve_any_problem (found_really_genuine, max_potential, max_genuine,
donno) first_time problems =
let
+ val kodkod_scala = Config.get ctxt KK.kodkod_scala
val max_potential = Int.max (0, max_potential)
val max_genuine = Int.max (0, max_genuine)
fun print_and_check genuine (j, bounds) =
@@ -702,7 +703,7 @@
if max_solutions <= 0 then
(found_really_genuine, 0, 0, donno)
else
- case KK.solve_any_problem debug overlord deadline max_threads
+ case KK.solve_any_problem kodkod_scala debug overlord deadline max_threads
max_solutions (map fst problems) of
KK.Normal ([], unsat_js, s) =>
(update_checked_problems problems unsat_js; show_kodkod_warning s;
--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Thu Nov 25 12:54:21 2021 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Thu Nov 25 19:56:01 2021 +0100
@@ -7,7 +7,7 @@
signature NITPICK_TESTS =
sig
- val run_all_tests : unit -> unit
+ val run_all_tests : Proof.context -> unit
end;
structure Nitpick_Tests : NITPICK_TESTS =
@@ -208,15 +208,17 @@
formula = formula}
end
-fun run_all_tests () =
+fun run_all_tests ctxt =
let
- val {debug, overlord, timeout, ...} = Nitpick_Commands.default_params \<^theory> []
+ val thy = Proof_Context.theory_of ctxt
+ val {debug, overlord, timeout, ...} = Nitpick_Commands.default_params thy []
+ val kodkod_scala = Config.get ctxt Kodkod.kodkod_scala
val deadline = Timeout.end_time timeout
val max_threads = 1
val max_solutions = 1
in
- case Kodkod.solve_any_problem debug overlord deadline max_threads max_solutions
- (map (problem_for_nut \<^context>) tests) of
+ case Kodkod.solve_any_problem kodkod_scala debug overlord deadline max_threads max_solutions
+ (map (problem_for_nut ctxt) tests) of
Kodkod.Normal ([], _, _) => ()
| _ => error "Tests failed"
end