always measure time for ATPs -- auto minimization relies on it
authorblanchet
Thu Sep 01 13:18:27 2011 +0200 (2011-09-01 ago)
changeset 446369a8de0397f65
parent 44635 3d046864ebe6
child 44637 13f86edf3db3
always measure time for ATPs -- auto minimization relies on it
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Sep 01 13:18:27 2011 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Sep 01 13:18:27 2011 +0200
     1.3 @@ -378,8 +378,7 @@
     1.4                   #> (Option.map (Config.put ATP_Systems.e_weight_method)
     1.5                         e_weight_method |> the_default I)
     1.6                   #> (Option.map (Config.put ATP_Systems.force_sos)
     1.7 -                       force_sos |> the_default I)
     1.8 -                 #> Config.put Sledgehammer_Provers.measure_run_time true)
     1.9 +                       force_sos |> the_default I))
    1.10      val params as {relevance_thresholds, max_relevant, slicing, ...} =
    1.11        Sledgehammer_Isar.default_params ctxt
    1.12            [("verbose", "true"),
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Sep 01 13:18:27 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Sep 01 13:18:27 2011 +0200
     2.3 @@ -62,7 +62,6 @@
     2.4  
     2.5    val dest_dir : string Config.T
     2.6    val problem_prefix : string Config.T
     2.7 -  val measure_run_time : bool Config.T
     2.8    val atp_lambda_translation : string Config.T
     2.9    val atp_full_names : bool Config.T
    2.10    val smt_triggers : bool Config.T
    2.11 @@ -339,8 +338,6 @@
    2.12    Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
    2.13  val problem_prefix =
    2.14    Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")
    2.15 -val measure_run_time =
    2.16 -  Attrib.setup_config_bool @{binding sledgehammer_measure_run_time} (K false)
    2.17  
    2.18  val atp_lambda_translation =
    2.19    Attrib.setup_config_string @{binding sledgehammer_atp_lambda_translation}
    2.20 @@ -506,9 +503,6 @@
    2.21    #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf
    2.22        is_exhaustive_finite)
    2.23  
    2.24 -fun int_opt_add (SOME m) (SOME n) = SOME (m + n)
    2.25 -  | int_opt_add _ _ = NONE
    2.26 -
    2.27  (* Important messages are important but not so important that users want to see
    2.28     them each time. *)
    2.29  val atp_important_message_keep_quotient = 10
    2.30 @@ -569,7 +563,6 @@
    2.31          Path.append (Path.explode dest_dir) problem_file_name
    2.32        else
    2.33          error ("No such directory: " ^ quote dest_dir ^ ".")
    2.34 -    val measure_run_time = verbose orelse Config.get ctxt measure_run_time
    2.35      val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
    2.36      fun split_time s =
    2.37        let
    2.38 @@ -581,7 +574,7 @@
    2.39          val num3 = as_num (digit ::: digit ::: (digit >> single))
    2.40          val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b)
    2.41          val as_time = Scan.read Symbol.stopper time o raw_explode
    2.42 -      in (output, as_time t) end
    2.43 +      in (output, as_time t |> the_default 0 (* can't happen *)) end
    2.44      fun run_on prob_file =
    2.45        case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of
    2.46          (home_var, _) :: _ =>
    2.47 @@ -666,11 +659,7 @@
    2.48                    File.shell_path command ^ " " ^
    2.49                    arguments ctxt full_proof extra slice_timeout weights ^ " " ^
    2.50                    File.shell_path prob_file
    2.51 -                val command =
    2.52 -                  (if measure_run_time then
    2.53 -                     "TIMEFORMAT='%3R'; { time " ^ core ^ " ; }"
    2.54 -                   else
    2.55 -                     "exec " ^ core) ^ " 2>&1"
    2.56 +                val command = "TIMEFORMAT='%3R'; { time " ^ core ^ " ; } 2>&1"
    2.57                  val _ =
    2.58                    atp_problem
    2.59                    |> tptp_lines_for_atp_problem format
    2.60 @@ -681,13 +670,13 @@
    2.61                      upto conjecture_offset + length hyp_ts + 1
    2.62                    |> map single
    2.63                  val ((output, msecs), (atp_proof, outcome)) =
    2.64 -                  TimeLimit.timeLimit generous_slice_timeout Isabelle_System.bash_output command
    2.65 +                  TimeLimit.timeLimit generous_slice_timeout
    2.66 +                                      Isabelle_System.bash_output command
    2.67                    |>> (if overlord then
    2.68                           prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
    2.69                         else
    2.70                           I)
    2.71 -                  |> fst
    2.72 -                  |> (if measure_run_time then split_time else rpair NONE)
    2.73 +                  |> fst |> split_time
    2.74                    |> (fn accum as (output, _) =>
    2.75                           (accum,
    2.76                            extract_tstplike_proof_and_outcome verbose complete
    2.77 @@ -696,7 +685,7 @@
    2.78                            handle UNRECOGNIZED_ATP_PROOF () =>
    2.79                                   ([], SOME ProofIncomplete)))
    2.80                    handle TimeLimit.TimeOut =>
    2.81 -                         (("", SOME (Time.toMilliseconds slice_timeout)),
    2.82 +                         (("", Time.toMilliseconds slice_timeout),
    2.83                            ([], SOME TimedOut))
    2.84                  val outcome =
    2.85                    case outcome of
    2.86 @@ -723,15 +712,15 @@
    2.87                    if Time.<= (time_left, Time.zeroTime) then
    2.88                      result
    2.89                    else
    2.90 -                    (run_slice slice time_left
    2.91 -                     |> (fn (stuff, (output, msecs, atp_proof, outcome)) =>
    2.92 -                            (stuff, (output, int_opt_add msecs0 msecs,
    2.93 -                                     atp_proof, outcome))))
    2.94 +                    run_slice slice time_left
    2.95 +                    |> (fn (stuff, (output, msecs, atp_proof, outcome)) =>
    2.96 +                           (stuff, (output, msecs0 + msecs, atp_proof,
    2.97 +                                    outcome)))
    2.98                  end
    2.99                | maybe_run_slice _ result = result
   2.100            in
   2.101              ((Symtab.empty, [], 0, Vector.fromList [], [], Symtab.empty),
   2.102 -             ("", SOME 0, [], SOME InternalError))
   2.103 +             ("", 0, [], SOME InternalError))
   2.104              |> fold maybe_run_slice actual_slices
   2.105            end
   2.106          else
   2.107 @@ -792,7 +781,7 @@
   2.108                in proof_text ctxt isar_proof isar_params one_line_params end,
   2.109             (if verbose then
   2.110                "\nATP real CPU time: " ^
   2.111 -              string_from_time (Time.fromMilliseconds (the msecs)) ^ "."
   2.112 +              string_from_time (Time.fromMilliseconds msecs) ^ "."
   2.113              else
   2.114                "") ^
   2.115             (if important_message <> "" then
   2.116 @@ -804,7 +793,7 @@
   2.117        | SOME failure =>
   2.118          ([], K (Failed_to_Play Metis), fn _ => string_for_failure failure, "")
   2.119    in
   2.120 -    {outcome = outcome, used_facts = used_facts, run_time_in_msecs = msecs,
   2.121 +    {outcome = outcome, used_facts = used_facts, run_time_in_msecs = SOME msecs,
   2.122       preplay = preplay, message = message, message_tail = message_tail}
   2.123    end
   2.124