added runtime information to sledgehammer
authorboehmes
Thu Sep 03 17:55:31 2009 +0200 (2009-09-03)
changeset 325101b56f8b1e5cc
parent 32509 9da37876874d
child 32511 43d2ac4aa2de
added runtime information to sledgehammer
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Tools/ATP_Manager/atp_manager.ML
src/HOL/Tools/ATP_Manager/atp_minimal.ML
src/HOL/Tools/ATP_Manager/atp_wrapper.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Sep 03 15:47:39 2009 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Sep 03 17:55:31 2009 +0200
     1.3 @@ -25,9 +25,6 @@
     1.4      val _ = done y
     1.5    in Exn.release z end
     1.6  
     1.7 -fun with_time true t = "succeeded (" ^ string_of_int t ^ ")"
     1.8 -  | with_time false t = "failed (" ^ string_of_int t ^ ")"
     1.9 -
    1.10  val proverK = "prover"
    1.11  val keepK = "keep"
    1.12  val metisK = "metis"
    1.13 @@ -50,12 +47,12 @@
    1.14      val prover = the (AtpManager.get_prover prover_name (Proof.theory_of st))
    1.15      val atp_timeout = AtpManager.get_timeout () 
    1.16      val atp = prover atp_timeout NONE NONE prover_name 1
    1.17 -    val (success, (message, thm_names), _, _, _) =
    1.18 +    val (success, (message, thm_names), time, _, _, _) =
    1.19        TimeLimit.timeLimit timeout atp (Proof.get_goal st)
    1.20 -  in (success, message, SOME thm_names) end
    1.21 -  handle ResHolClause.TOO_TRIVIAL => (true, "trivial", SOME [])
    1.22 -       | TimeLimit.TimeOut => (false, "time out", NONE)
    1.23 -       | ERROR msg => (false, "error: " ^ msg, NONE)
    1.24 +  in if success then (message, SOME (time, thm_names)) else (message, NONE) end
    1.25 +  handle ResHolClause.TOO_TRIVIAL => ("trivial", SOME (0, []))
    1.26 +       | TimeLimit.TimeOut => ("time out", NONE)
    1.27 +       | ERROR msg => ("error: " ^ msg, NONE)
    1.28  
    1.29  in
    1.30  
    1.31 @@ -65,16 +62,20 @@
    1.32        AList.lookup (op =) args proverK
    1.33        |> the_default (hd (space_explode " " (AtpManager.get_atps ())))
    1.34      val dir = AList.lookup (op =) args keepK
    1.35 -    val ((success, msg, thm_names), time) =
    1.36 -      safe init done (Mirabelle.cpu_time (run prover_name timeout st)) dir
    1.37 -    fun sh_log s = log ("sledgehammer: " ^ with_time success time ^ " [" ^
    1.38 -      prover_name ^ "]" ^ s)
    1.39 -    val _ = if success then sh_log (":\n" ^ msg) else sh_log ""
    1.40 -  in if success then thm_names else NONE end
    1.41 +    val (msg, result) = safe init done (run prover_name timeout st) dir
    1.42 +    val _ =
    1.43 +      if is_some result
    1.44 +      then log ("sledgehammer: succeeded (" ^ string_of_int (fst (the result)) ^
    1.45 +        ") [" ^ prover_name ^ "]:\n" ^ msg)
    1.46 +      else log ("sledgehammer: failed: " ^ msg)
    1.47 +  in Option.map snd result end
    1.48  
    1.49  end
    1.50  
    1.51  
    1.52 +fun with_time true t = "succeeded (" ^ string_of_int t ^ ")"
    1.53 +  | with_time false t = "failed (" ^ string_of_int t ^ ")"
    1.54 +
    1.55  fun run_metis (args, st, timeout, log) thm_names =
    1.56    let
    1.57      fun get_thms ctxt = maps (thms_of_name ctxt)
     2.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Thu Sep 03 15:47:39 2009 +0200
     2.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Thu Sep 03 17:55:31 2009 +0200
     2.3 @@ -24,7 +24,7 @@
     2.4    type prover = int -> (thm * (string * int)) list option ->
     2.5      (thm * (string * int)) list option -> string -> int ->
     2.6      Proof.context * (thm list * thm) ->
     2.7 -    bool * (string * string list) * string * string vector * (thm * (string * int)) list
     2.8 +    bool * (string * string list) * int * string * string vector * (thm * (string * int)) list
     2.9    val add_prover: string -> prover -> theory -> theory
    2.10    val print_provers: theory -> unit
    2.11    val get_prover: string -> theory -> prover option
    2.12 @@ -305,7 +305,7 @@
    2.13  type prover = int -> (thm * (string * int)) list option ->
    2.14    (thm * (string * int)) list option -> string -> int ->
    2.15    Proof.context * (thm list * thm) ->
    2.16 -  bool * (string * string list) * string * string vector * (thm * (string * int)) list
    2.17 +  bool * (string * string list) * int * string * string vector * (thm * (string * int)) list
    2.18  
    2.19  fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
    2.20  
    2.21 @@ -345,7 +345,7 @@
    2.22            let
    2.23              val _ = register birthtime deadtime (Thread.self (), desc)
    2.24              val result =
    2.25 -              let val (success, (message, _), _, _, _) =
    2.26 +              let val (success, (message, _), _, _, _, _) =
    2.27                  prover (get_timeout ()) NONE NONE name i (Proof.get_goal proof_state)
    2.28                in (success, message) end
    2.29                handle ResHolClause.TOO_TRIVIAL
     3.1 --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Thu Sep 03 15:47:39 2009 +0200
     3.2 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Thu Sep 03 17:55:31 2009 +0200
     3.3 @@ -83,7 +83,7 @@
     3.4     ("# Cannot determine problem status within resource limit", Timeout),
     3.5     ("Error", Error)]
     3.6  
     3.7 -fun produce_answer (success, message, result_string, thm_name_vec, filtered) =
     3.8 +fun produce_answer (success, message, _, result_string, thm_name_vec, filtered) =
     3.9    if success then
    3.10      (Success (Vector.foldr op:: [] thm_name_vec, filtered), result_string)
    3.11    else
     4.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Thu Sep 03 15:47:39 2009 +0200
     4.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Thu Sep 03 17:55:31 2009 +0200
     4.3 @@ -79,19 +79,29 @@
     4.4        preparer goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy
     4.5  
     4.6      (* write out problem file and call prover *)
     4.7 -    fun cmd_line probfile = space_implode " " ["exec", File.shell_path cmd,
     4.8 -      args, File.platform_path probfile]
     4.9 +    fun cmd_line probfile = "TIMEFORMAT='%3U'; ((time " ^ space_implode " "
    4.10 +      [File.shell_path cmd, args, File.platform_path probfile] ^ ") 2>&1)"
    4.11 +    fun split_time s =
    4.12 +      let
    4.13 +        val split = String.tokens (fn c => str c = "\n")
    4.14 +        val (proof, t) = s |> split |> split_last |> apfst cat_lines
    4.15 +        val num = Scan.many1 Symbol.is_ascii_digit >> (fst o read_int)
    4.16 +        val time = num --| Scan.$$ "." -- num >> (fn (a, b) => a * 1000 + b)
    4.17 +        val as_time = the_default 0 o Scan.read Symbol.stopper time o explode
    4.18 +      in (proof, as_time t) end
    4.19      fun run_on probfile =
    4.20        if File.exists cmd
    4.21 -      then writer probfile clauses |> pair (system_out (cmd_line probfile))
    4.22 +      then
    4.23 +        writer probfile clauses
    4.24 +        |> pair (apfst split_time (system_out (cmd_line probfile)))
    4.25        else error ("Bad executable: " ^ Path.implode cmd)
    4.26  
    4.27      (* if problemfile has not been exported, delete problemfile; otherwise export proof, too *)
    4.28      fun cleanup probfile = if destdir' = "" then File.rm probfile else ()
    4.29 -    fun export probfile ((proof, _), _) = if destdir' = "" then ()
    4.30 +    fun export probfile (((proof, _), _), _) = if destdir' = "" then ()
    4.31        else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof
    4.32  
    4.33 -    val ((proof, rc), conj_pos) = with_path cleanup export run_on
    4.34 +    val (((proof, time), rc), conj_pos) = with_path cleanup export run_on
    4.35        (prob_pathname subgoalno)
    4.36  
    4.37      (* check for success and print out some information on failure *)
    4.38 @@ -103,7 +113,7 @@
    4.39        else apfst (fn s => "Try this command: " ^ s)
    4.40          (produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoalno))
    4.41      val _ = Output.debug (fn () => "Sledgehammer response (rc = " ^ string_of_int rc ^ "):\n" ^ proof)
    4.42 -  in (success, message, proof, thm_names, the_filtered_clauses) end;
    4.43 +  in (success, message, time, proof, thm_names, the_filtered_clauses) end;
    4.44  
    4.45  
    4.46