system options for Isabelle/HOL proof tools;
authorwenzelm
Fri Jul 12 23:45:05 2013 +0200 (2013-07-12)
changeset 52639df830310e550
parent 52638 c1adf8b2eccf
child 52640 38679321b251
system options for Isabelle/HOL proof tools;
etc/components
src/HOL/Mutabelle/MutabelleExtra.thy
src/HOL/Mutabelle/lib/Tools/mutabelle
src/HOL/Mutabelle/mutabelle_extra.ML
src/HOL/Tools/Nitpick/nitpick_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/etc/options
src/HOL/Tools/try0.ML
src/Tools/quickcheck.ML
src/Tools/solve_direct.ML
src/Tools/try.ML
     1.1 --- a/etc/components	Fri Jul 12 22:49:20 2013 +0200
     1.2 +++ b/etc/components	Fri Jul 12 23:45:05 2013 +0200
     1.3 @@ -5,6 +5,7 @@
     1.4  src/HOL/Mirabelle
     1.5  src/HOL/Mutabelle
     1.6  src/HOL/Library/Sum_of_Squares
     1.7 +src/HOL/Tools
     1.8  src/HOL/Tools/ATP
     1.9  src/HOL/Tools/Sledgehammer/MaSh
    1.10  src/HOL/Tools/SMT
     2.1 --- a/src/HOL/Mutabelle/MutabelleExtra.thy	Fri Jul 12 22:49:20 2013 +0200
     2.2 +++ b/src/HOL/Mutabelle/MutabelleExtra.thy	Fri Jul 12 23:45:05 2013 +0200
     2.3 @@ -26,7 +26,6 @@
     2.4  nitpick_params [timeout = 5, sat_solver = MiniSat, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
     2.5  refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat]
     2.6  *)
     2.7 -ML {* Try.auto_time_limit := 10.0 *}
     2.8  
     2.9  ML {* val mtds = [
    2.10    MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "random",
     3.1 --- a/src/HOL/Mutabelle/lib/Tools/mutabelle	Fri Jul 12 22:49:20 2013 +0200
     3.2 +++ b/src/HOL/Mutabelle/lib/Tools/mutabelle	Fri Jul 12 23:45:05 2013 +0200
     3.3 @@ -133,7 +133,8 @@
     3.4  
     3.5  # execution
     3.6  
     3.7 -"$ISABELLE_PROCESS" -e 'use_thy "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test"' -q "$MUTABELLE_LOGIC" > "$MUTABELLE_OUTPUT_PATH/err" 2>&1
     3.8 +"$ISABELLE_PROCESS" -o auto_time_limit=10.0 \
     3.9 +  -e 'use_thy "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test"' -q "$MUTABELLE_LOGIC" > "$MUTABELLE_OUTPUT_PATH/err" 2>&1
    3.10  
    3.11  
    3.12  [ $? -ne 0 ] && echo "isabelle processing of mutabelle failed"
     4.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Jul 12 22:49:20 2013 +0200
     4.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Jul 12 23:45:05 2013 +0200
     4.3 @@ -120,7 +120,7 @@
     4.4              | SOME _ => (GenuineCex, Quickcheck.timings_of result)
     4.5            end) ()
     4.6    handle TimeLimit.TimeOut =>
     4.7 -         (Timeout, [("timelimit", Real.floor (!Try.auto_time_limit))])
     4.8 +         (Timeout, [("timelimit", Real.floor (Options.default_real @{option auto_time_limit})])
     4.9  
    4.10  fun quickcheck_mtd change_options quickcheck_generator =
    4.11    ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options)
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Fri Jul 12 22:49:20 2013 +0200
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Fri Jul 12 23:45:05 2013 +0200
     5.3 @@ -12,7 +12,6 @@
     5.4  
     5.5    val nitpickN : string
     5.6    val nitpick_paramsN : string
     5.7 -  val auto : bool Unsynchronized.ref
     5.8    val default_params : theory -> (string * string) list -> params
     5.9    val setup : theory -> theory
    5.10  end;
    5.11 @@ -29,16 +28,14 @@
    5.12  val nitpickN = "nitpick"
    5.13  val nitpick_paramsN = "nitpick_params"
    5.14  
    5.15 -val auto = Unsynchronized.ref false
    5.16 -
    5.17  (* Maximum number of scopes for Auto Nitpick. Be frugal since it has to share
    5.18     its time slot with several other automatic tools. *)
    5.19  val auto_try_max_scopes = 6
    5.20  
    5.21  val _ =
    5.22 -  ProofGeneral.preference_bool ProofGeneral.category_tracing
    5.23 +  ProofGeneral.preference_option ProofGeneral.category_tracing
    5.24      NONE
    5.25 -    auto
    5.26 +    @{option auto_nitpick}
    5.27      "auto-nitpick"
    5.28      "Run Nitpick automatically"
    5.29  
    5.30 @@ -402,6 +399,6 @@
    5.31  
    5.32  fun try_nitpick auto = pick_nits [] (if auto then Auto_Try else Try) 1 0
    5.33  
    5.34 -val setup = Try.register_tool (nitpickN, (50, auto, try_nitpick))
    5.35 +val setup = Try.register_tool (nitpickN, (50, @{option auto_nitpick}, try_nitpick))
    5.36  
    5.37  end;
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 12 22:49:20 2013 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 12 23:45:05 2013 +0200
     6.3 @@ -8,7 +8,6 @@
     6.4  sig
     6.5    type params = Sledgehammer_Provers.params
     6.6  
     6.7 -  val auto : bool Unsynchronized.ref
     6.8    val provers : string Unsynchronized.ref
     6.9    val timeout : int Unsynchronized.ref
    6.10    val default_params : Proof.context -> (string * string) list -> params
    6.11 @@ -42,12 +41,10 @@
    6.12  val running_learnersN = "running_learners"
    6.13  val refresh_tptpN = "refresh_tptp"
    6.14  
    6.15 -val auto = Unsynchronized.ref false
    6.16 -
    6.17  val _ =
    6.18 -  ProofGeneral.preference_bool ProofGeneral.category_tracing
    6.19 +  ProofGeneral.preference_option ProofGeneral.category_tracing
    6.20      NONE
    6.21 -    auto
    6.22 +    @{option auto_sledgehammer}
    6.23      "auto-sledgehammer"
    6.24      "Run Sledgehammer automatically"
    6.25  
    6.26 @@ -489,6 +486,6 @@
    6.27                       (minimize_command [] i) state
    6.28    end
    6.29  
    6.30 -val setup = Try.register_tool (sledgehammerN, (40, auto, try_sledgehammer))
    6.31 +val setup = Try.register_tool (sledgehammerN, (40, @{option auto_sledgehammer}, try_sledgehammer))
    6.32  
    6.33  end;
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Tools/etc/options	Fri Jul 12 23:45:05 2013 +0200
     7.3 @@ -0,0 +1,22 @@
     7.4 +(* :mode=isabelle-options: *)
     7.5 +
     7.6 +section {* Isabelle/HOL proof tools *}
     7.7 +
     7.8 +public option auto_time_limit : real = 4.0
     7.9 +  -- "time limit for automatically tried tools (seconds > 0)"
    7.10 +
    7.11 +public option auto_nitpick : bool = false
    7.12 +  -- "run Nitpick automatically"
    7.13 +
    7.14 +public option auto_sledgehammer : bool = false
    7.15 +  -- "run Sledgehammer automatically"
    7.16 +
    7.17 +public option auto_try0 : bool = false
    7.18 +  -- "try standard proof methods automatically"
    7.19 +
    7.20 +public option auto_quickcheck : bool = false
    7.21 +  -- "run Quickcheck automatically"
    7.22 +
    7.23 +public option auto_solve_direct : bool = false
    7.24 +  -- "run solve_direct automatically"
    7.25 +
     8.1 --- a/src/HOL/Tools/try0.ML	Fri Jul 12 22:49:20 2013 +0200
     8.2 +++ b/src/HOL/Tools/try0.ML	Fri Jul 12 23:45:05 2013 +0200
     8.3 @@ -8,7 +8,6 @@
     8.4  sig
     8.5    val try0N : string
     8.6    val noneN : string
     8.7 -  val auto : bool Unsynchronized.ref
     8.8    val try0 :
     8.9      Time.time option -> string list * string list * string list * string list
    8.10      -> Proof.state -> bool
    8.11 @@ -24,12 +23,10 @@
    8.12  
    8.13  val noneN = "none"
    8.14  
    8.15 -val auto = Unsynchronized.ref false
    8.16 -
    8.17  val _ =
    8.18 -  ProofGeneral.preference_bool ProofGeneral.category_tracing
    8.19 +  ProofGeneral.preference_option ProofGeneral.category_tracing
    8.20      NONE
    8.21 -    auto
    8.22 +    @{option auto_try0}
    8.23      "auto-try0"
    8.24      "Try standard proof methods"
    8.25  
    8.26 @@ -196,6 +193,6 @@
    8.27  fun try_try0 auto =
    8.28    do_try0 (if auto then Auto_Try else Try) NONE ([], [], [], [])
    8.29  
    8.30 -val setup = Try.register_tool (try0N, (30, auto, try_try0))
    8.31 +val setup = Try.register_tool (try0N, (30, @{option auto_try0}, try_try0))
    8.32  
    8.33  end;
     9.1 --- a/src/Tools/quickcheck.ML	Fri Jul 12 22:49:20 2013 +0200
     9.2 +++ b/src/Tools/quickcheck.ML	Fri Jul 12 23:45:05 2013 +0200
     9.3 @@ -12,7 +12,6 @@
     9.4    val unknownN: string
     9.5    val setup: theory -> theory
     9.6    (*configuration*)
     9.7 -  val auto: bool Unsynchronized.ref
     9.8    val batch_tester : string Config.T
     9.9    val size : int Config.T
    9.10    val iterations : int Config.T
    9.11 @@ -94,12 +93,10 @@
    9.12  
    9.13  (* preferences *)
    9.14  
    9.15 -val auto = Unsynchronized.ref false;
    9.16 -
    9.17  val _ =
    9.18 -  ProofGeneral.preference_bool ProofGeneral.category_tracing
    9.19 +  ProofGeneral.preference_option ProofGeneral.category_tracing
    9.20      (SOME "true")
    9.21 -    auto
    9.22 +    @{option auto_quickcheck}
    9.23      "auto-quickcheck"
    9.24      "Run Quickcheck automatically";
    9.25  
    9.26 @@ -567,8 +564,7 @@
    9.27    end
    9.28    |> `(fn (outcome_code, _) => outcome_code = genuineN);
    9.29  
    9.30 -val setup = Try.register_tool (quickcheckN, (20, auto, try_quickcheck));
    9.31 +val setup = Try.register_tool (quickcheckN, (20, @{option auto_quickcheck}, try_quickcheck));
    9.32  
    9.33  end;
    9.34  
    9.35 -val auto_quickcheck = Quickcheck.auto;
    10.1 --- a/src/Tools/solve_direct.ML	Fri Jul 12 22:49:20 2013 +0200
    10.2 +++ b/src/Tools/solve_direct.ML	Fri Jul 12 23:45:05 2013 +0200
    10.3 @@ -14,7 +14,6 @@
    10.4    val someN: string
    10.5    val noneN: string
    10.6    val unknownN: string
    10.7 -  val auto: bool Unsynchronized.ref
    10.8    val max_solutions: int Unsynchronized.ref
    10.9    val solve_direct: Proof.state -> bool * (string * Proof.state)
   10.10    val setup: theory -> theory
   10.11 @@ -33,13 +32,12 @@
   10.12  
   10.13  (* preferences *)
   10.14  
   10.15 -val auto = Unsynchronized.ref false;
   10.16  val max_solutions = Unsynchronized.ref 5;
   10.17  
   10.18  val _ =
   10.19 -  ProofGeneral.preference_bool ProofGeneral.category_tracing
   10.20 +  ProofGeneral.preference_option ProofGeneral.category_tracing
   10.21      (SOME "true")
   10.22 -    auto
   10.23 +    @{option auto_solve_direct}
   10.24      "auto-solve-direct"
   10.25      ("Run " ^ quote solve_directN ^ " automatically");
   10.26  
   10.27 @@ -117,6 +115,6 @@
   10.28  
   10.29  fun try_solve_direct auto = do_solve_direct (if auto then Auto_Try else Try)
   10.30  
   10.31 -val setup = Try.register_tool (solve_directN, (10, auto, try_solve_direct));
   10.32 +val setup = Try.register_tool (solve_directN, (10, @{option auto_solve_direct}, try_solve_direct));
   10.33  
   10.34  end;
    11.1 --- a/src/Tools/try.ML	Fri Jul 12 22:49:20 2013 +0200
    11.2 +++ b/src/Tools/try.ML	Fri Jul 12 23:45:05 2013 +0200
    11.3 @@ -7,11 +7,9 @@
    11.4  signature TRY =
    11.5  sig
    11.6    type tool =
    11.7 -    string * (int * bool Unsynchronized.ref
    11.8 -              * (bool -> Proof.state -> bool * (string * Proof.state)))
    11.9 +    string * (int * string * (bool -> Proof.state -> bool * (string * Proof.state)))
   11.10  
   11.11    val tryN : string
   11.12 -  val auto_time_limit: real Unsynchronized.ref
   11.13  
   11.14    val serial_commas : string -> string list -> string list
   11.15    val subgoal_count : Proof.state -> int
   11.16 @@ -24,20 +22,17 @@
   11.17  struct
   11.18  
   11.19  type tool =
   11.20 -  string * (int * bool Unsynchronized.ref
   11.21 -            * (bool -> Proof.state -> bool * (string * Proof.state)))
   11.22 +  string * (int * string * (bool -> Proof.state -> bool * (string * Proof.state)))
   11.23  
   11.24  val tryN = "try"
   11.25  
   11.26  
   11.27  (* preferences *)
   11.28  
   11.29 -val auto_time_limit = Unsynchronized.ref 4.0
   11.30 -
   11.31  val _ =
   11.32 -  ProofGeneral.preference_real ProofGeneral.category_tracing
   11.33 +  ProofGeneral.preference_option ProofGeneral.category_tracing
   11.34      NONE
   11.35 -    auto_time_limit
   11.36 +    @{option auto_time_limit}
   11.37      "auto-try-time-limit"
   11.38      "Time limit for automatically tried tools (in seconds)"
   11.39  
   11.40 @@ -98,7 +93,7 @@
   11.41  
   11.42  fun auto_try state =
   11.43    get_tools (Proof.theory_of state)
   11.44 -  |> map_filter (fn (_, (_, auto, tool)) => if !auto then SOME tool else NONE)
   11.45 +  |> map_filter (fn (_, (_, auto, tool)) => if Options.default_bool auto then SOME tool else NONE)
   11.46    |> Par_List.get_some (fn tool =>
   11.47                             case try (tool true) state of
   11.48                               SOME (true, (_, state)) => SOME state
   11.49 @@ -106,10 +101,14 @@
   11.50    |> the_default state
   11.51  
   11.52  val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
   11.53 -  if interact andalso not (!Toplevel.quiet) andalso !auto_time_limit > 0.0 then
   11.54 -    TimeLimit.timeLimit (seconds (!auto_time_limit)) auto_try state
   11.55 -    handle TimeLimit.TimeOut => state
   11.56 -  else
   11.57 -    state))
   11.58 +  let
   11.59 +    val auto_time_limit = Options.default_real @{option auto_time_limit}
   11.60 +  in
   11.61 +    if interact andalso not (!Toplevel.quiet) andalso auto_time_limit > 0.0 then
   11.62 +      TimeLimit.timeLimit (seconds auto_time_limit) auto_try state
   11.63 +      handle TimeLimit.TimeOut => state
   11.64 +    else
   11.65 +      state
   11.66 +  end))
   11.67  
   11.68  end;