# HG changeset patch
# User wenzelm
# Date 1373665505 -7200
# Node ID df830310e550401ae749c548e242055e2d86bc62
# Parent  c1adf8b2eccf3c7e4d14d0681c1a5f10759594de
system options for Isabelle/HOL proof tools;

diff -r c1adf8b2eccf -r df830310e550 etc/components
--- 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
diff -r c1adf8b2eccf -r df830310e550 src/HOL/Mutabelle/MutabelleExtra.thy
--- 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",
diff -r c1adf8b2eccf -r df830310e550 src/HOL/Mutabelle/lib/Tools/mutabelle
--- 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"
diff -r c1adf8b2eccf -r df830310e550 src/HOL/Mutabelle/mutabelle_extra.ML
--- 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)
diff -r c1adf8b2eccf -r df830310e550 src/HOL/Tools/Nitpick/nitpick_isar.ML
--- 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;
diff -r c1adf8b2eccf -r df830310e550 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- 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;
diff -r c1adf8b2eccf -r df830310e550 src/HOL/Tools/etc/options
--- /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"
+
diff -r c1adf8b2eccf -r df830310e550 src/HOL/Tools/try0.ML
--- 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;
diff -r c1adf8b2eccf -r df830310e550 src/Tools/quickcheck.ML
--- 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;
diff -r c1adf8b2eccf -r df830310e550 src/Tools/solve_direct.ML
--- 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;
diff -r c1adf8b2eccf -r df830310e550 src/Tools/try.ML
--- 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;