--- a/etc/components Fri Jul 12 22:49:20 2013 +0200
+++ b/etc/components Fri Jul 12 23:45:05 2013 +0200
@@ -5,6 +5,7 @@
src/HOL/Mirabelle
src/HOL/Mutabelle
src/HOL/Library/Sum_of_Squares
+src/HOL/Tools
src/HOL/Tools/ATP
src/HOL/Tools/Sledgehammer/MaSh
src/HOL/Tools/SMT
--- a/src/HOL/Mutabelle/MutabelleExtra.thy Fri Jul 12 22:49:20 2013 +0200
+++ b/src/HOL/Mutabelle/MutabelleExtra.thy Fri Jul 12 23:45:05 2013 +0200
@@ -26,7 +26,6 @@
nitpick_params [timeout = 5, sat_solver = MiniSat, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat]
*)
-ML {* Try.auto_time_limit := 10.0 *}
ML {* val mtds = [
MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "random",
--- a/src/HOL/Mutabelle/lib/Tools/mutabelle Fri Jul 12 22:49:20 2013 +0200
+++ b/src/HOL/Mutabelle/lib/Tools/mutabelle Fri Jul 12 23:45:05 2013 +0200
@@ -133,7 +133,8 @@
# execution
-"$ISABELLE_PROCESS" -e 'use_thy "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test"' -q "$MUTABELLE_LOGIC" > "$MUTABELLE_OUTPUT_PATH/err" 2>&1
+"$ISABELLE_PROCESS" -o auto_time_limit=10.0 \
+ -e 'use_thy "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test"' -q "$MUTABELLE_LOGIC" > "$MUTABELLE_OUTPUT_PATH/err" 2>&1
[ $? -ne 0 ] && echo "isabelle processing of mutabelle failed"
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri Jul 12 22:49:20 2013 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri Jul 12 23:45:05 2013 +0200
@@ -120,7 +120,7 @@
| SOME _ => (GenuineCex, Quickcheck.timings_of result)
end) ()
handle TimeLimit.TimeOut =>
- (Timeout, [("timelimit", Real.floor (!Try.auto_time_limit))])
+ (Timeout, [("timelimit", Real.floor (Options.default_real @{option auto_time_limit})])
fun quickcheck_mtd change_options quickcheck_generator =
("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options)
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri Jul 12 22:49:20 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri Jul 12 23:45:05 2013 +0200
@@ -12,7 +12,6 @@
val nitpickN : string
val nitpick_paramsN : string
- val auto : bool Unsynchronized.ref
val default_params : theory -> (string * string) list -> params
val setup : theory -> theory
end;
@@ -29,16 +28,14 @@
val nitpickN = "nitpick"
val nitpick_paramsN = "nitpick_params"
-val auto = Unsynchronized.ref false
-
(* Maximum number of scopes for Auto Nitpick. Be frugal since it has to share
its time slot with several other automatic tools. *)
val auto_try_max_scopes = 6
val _ =
- ProofGeneral.preference_bool ProofGeneral.category_tracing
+ ProofGeneral.preference_option ProofGeneral.category_tracing
NONE
- auto
+ @{option auto_nitpick}
"auto-nitpick"
"Run Nitpick automatically"
@@ -402,6 +399,6 @@
fun try_nitpick auto = pick_nits [] (if auto then Auto_Try else Try) 1 0
-val setup = Try.register_tool (nitpickN, (50, auto, try_nitpick))
+val setup = Try.register_tool (nitpickN, (50, @{option auto_nitpick}, try_nitpick))
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 12 22:49:20 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 12 23:45:05 2013 +0200
@@ -8,7 +8,6 @@
sig
type params = Sledgehammer_Provers.params
- val auto : bool Unsynchronized.ref
val provers : string Unsynchronized.ref
val timeout : int Unsynchronized.ref
val default_params : Proof.context -> (string * string) list -> params
@@ -42,12 +41,10 @@
val running_learnersN = "running_learners"
val refresh_tptpN = "refresh_tptp"
-val auto = Unsynchronized.ref false
-
val _ =
- ProofGeneral.preference_bool ProofGeneral.category_tracing
+ ProofGeneral.preference_option ProofGeneral.category_tracing
NONE
- auto
+ @{option auto_sledgehammer}
"auto-sledgehammer"
"Run Sledgehammer automatically"
@@ -489,6 +486,6 @@
(minimize_command [] i) state
end
-val setup = Try.register_tool (sledgehammerN, (40, auto, try_sledgehammer))
+val setup = Try.register_tool (sledgehammerN, (40, @{option auto_sledgehammer}, try_sledgehammer))
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/etc/options Fri Jul 12 23:45:05 2013 +0200
@@ -0,0 +1,22 @@
+(* :mode=isabelle-options: *)
+
+section {* Isabelle/HOL proof tools *}
+
+public option auto_time_limit : real = 4.0
+ -- "time limit for automatically tried tools (seconds > 0)"
+
+public option auto_nitpick : bool = false
+ -- "run Nitpick automatically"
+
+public option auto_sledgehammer : bool = false
+ -- "run Sledgehammer automatically"
+
+public option auto_try0 : bool = false
+ -- "try standard proof methods automatically"
+
+public option auto_quickcheck : bool = false
+ -- "run Quickcheck automatically"
+
+public option auto_solve_direct : bool = false
+ -- "run solve_direct automatically"
+
--- a/src/HOL/Tools/try0.ML Fri Jul 12 22:49:20 2013 +0200
+++ b/src/HOL/Tools/try0.ML Fri Jul 12 23:45:05 2013 +0200
@@ -8,7 +8,6 @@
sig
val try0N : string
val noneN : string
- val auto : bool Unsynchronized.ref
val try0 :
Time.time option -> string list * string list * string list * string list
-> Proof.state -> bool
@@ -24,12 +23,10 @@
val noneN = "none"
-val auto = Unsynchronized.ref false
-
val _ =
- ProofGeneral.preference_bool ProofGeneral.category_tracing
+ ProofGeneral.preference_option ProofGeneral.category_tracing
NONE
- auto
+ @{option auto_try0}
"auto-try0"
"Try standard proof methods"
@@ -196,6 +193,6 @@
fun try_try0 auto =
do_try0 (if auto then Auto_Try else Try) NONE ([], [], [], [])
-val setup = Try.register_tool (try0N, (30, auto, try_try0))
+val setup = Try.register_tool (try0N, (30, @{option auto_try0}, try_try0))
end;
--- a/src/Tools/quickcheck.ML Fri Jul 12 22:49:20 2013 +0200
+++ b/src/Tools/quickcheck.ML Fri Jul 12 23:45:05 2013 +0200
@@ -12,7 +12,6 @@
val unknownN: string
val setup: theory -> theory
(*configuration*)
- val auto: bool Unsynchronized.ref
val batch_tester : string Config.T
val size : int Config.T
val iterations : int Config.T
@@ -94,12 +93,10 @@
(* preferences *)
-val auto = Unsynchronized.ref false;
-
val _ =
- ProofGeneral.preference_bool ProofGeneral.category_tracing
+ ProofGeneral.preference_option ProofGeneral.category_tracing
(SOME "true")
- auto
+ @{option auto_quickcheck}
"auto-quickcheck"
"Run Quickcheck automatically";
@@ -567,8 +564,7 @@
end
|> `(fn (outcome_code, _) => outcome_code = genuineN);
-val setup = Try.register_tool (quickcheckN, (20, auto, try_quickcheck));
+val setup = Try.register_tool (quickcheckN, (20, @{option auto_quickcheck}, try_quickcheck));
end;
-val auto_quickcheck = Quickcheck.auto;
--- a/src/Tools/solve_direct.ML Fri Jul 12 22:49:20 2013 +0200
+++ b/src/Tools/solve_direct.ML Fri Jul 12 23:45:05 2013 +0200
@@ -14,7 +14,6 @@
val someN: string
val noneN: string
val unknownN: string
- val auto: bool Unsynchronized.ref
val max_solutions: int Unsynchronized.ref
val solve_direct: Proof.state -> bool * (string * Proof.state)
val setup: theory -> theory
@@ -33,13 +32,12 @@
(* preferences *)
-val auto = Unsynchronized.ref false;
val max_solutions = Unsynchronized.ref 5;
val _ =
- ProofGeneral.preference_bool ProofGeneral.category_tracing
+ ProofGeneral.preference_option ProofGeneral.category_tracing
(SOME "true")
- auto
+ @{option auto_solve_direct}
"auto-solve-direct"
("Run " ^ quote solve_directN ^ " automatically");
@@ -117,6 +115,6 @@
fun try_solve_direct auto = do_solve_direct (if auto then Auto_Try else Try)
-val setup = Try.register_tool (solve_directN, (10, auto, try_solve_direct));
+val setup = Try.register_tool (solve_directN, (10, @{option auto_solve_direct}, try_solve_direct));
end;
--- a/src/Tools/try.ML Fri Jul 12 22:49:20 2013 +0200
+++ b/src/Tools/try.ML Fri Jul 12 23:45:05 2013 +0200
@@ -7,11 +7,9 @@
signature TRY =
sig
type tool =
- string * (int * bool Unsynchronized.ref
- * (bool -> Proof.state -> bool * (string * Proof.state)))
+ string * (int * string * (bool -> Proof.state -> bool * (string * Proof.state)))
val tryN : string
- val auto_time_limit: real Unsynchronized.ref
val serial_commas : string -> string list -> string list
val subgoal_count : Proof.state -> int
@@ -24,20 +22,17 @@
struct
type tool =
- string * (int * bool Unsynchronized.ref
- * (bool -> Proof.state -> bool * (string * Proof.state)))
+ string * (int * string * (bool -> Proof.state -> bool * (string * Proof.state)))
val tryN = "try"
(* preferences *)
-val auto_time_limit = Unsynchronized.ref 4.0
-
val _ =
- ProofGeneral.preference_real ProofGeneral.category_tracing
+ ProofGeneral.preference_option ProofGeneral.category_tracing
NONE
- auto_time_limit
+ @{option auto_time_limit}
"auto-try-time-limit"
"Time limit for automatically tried tools (in seconds)"
@@ -98,7 +93,7 @@
fun auto_try state =
get_tools (Proof.theory_of state)
- |> map_filter (fn (_, (_, auto, tool)) => if !auto then SOME tool else NONE)
+ |> map_filter (fn (_, (_, auto, tool)) => if Options.default_bool auto then SOME tool else NONE)
|> Par_List.get_some (fn tool =>
case try (tool true) state of
SOME (true, (_, state)) => SOME state
@@ -106,10 +101,14 @@
|> the_default state
val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
- if interact andalso not (!Toplevel.quiet) andalso !auto_time_limit > 0.0 then
- TimeLimit.timeLimit (seconds (!auto_time_limit)) auto_try state
- handle TimeLimit.TimeOut => state
- else
- state))
+ let
+ val auto_time_limit = Options.default_real @{option auto_time_limit}
+ in
+ if interact andalso not (!Toplevel.quiet) andalso auto_time_limit > 0.0 then
+ TimeLimit.timeLimit (seconds auto_time_limit) auto_try state
+ handle TimeLimit.TimeOut => state
+ else
+ state
+ end))
end;