# HG changeset patch # User wenzelm # Date 1637866561 -3600 # Node ID 90242c744a1a5e86696648a79e37d0860e5371c4 # Parent ace8be1881e101d796bbc2b13893f9502b07002d maintain option kodkod_scala within theory context, to allow local modification; diff -r ace8be1881e1 -r 90242c744a1a NEWS --- 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. diff -r ace8be1881e1 -r 90242c744a1a src/HOL/Nitpick_Examples/Tests_Nits.thy --- 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 \() |> getenv "KODKODI" <> "" ? Nitpick_Tests.run_all_tests\ +ML \if getenv "KODKODI" = "" then () else Nitpick_Tests.run_all_tests \<^context>\ end diff -r ace8be1881e1 -r 90242c744a1a src/HOL/Nitpick_Examples/minipick.ML --- 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" diff -r ace8be1881e1 -r 90242c744a1a src/HOL/Tools/Nitpick/kodkod.ML --- 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>\kodkod_max_threads\ else max_threads0 - val external_process = - not (Options.default_bool \<^system_option>\kodkod_scala\) 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>\kodkod_scala\, \<^here>) + end; diff -r ace8be1881e1 -r 90242c744a1a src/HOL/Tools/Nitpick/nitpick.ML --- 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; diff -r ace8be1881e1 -r 90242c744a1a src/HOL/Tools/Nitpick/nitpick_tests.ML --- 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