--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Sep 03 15:47:39 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Sep 03 17:55:31 2009 +0200
@@ -25,9 +25,6 @@
val _ = done y
in Exn.release z end
-fun with_time true t = "succeeded (" ^ string_of_int t ^ ")"
- | with_time false t = "failed (" ^ string_of_int t ^ ")"
-
val proverK = "prover"
val keepK = "keep"
val metisK = "metis"
@@ -50,12 +47,12 @@
val prover = the (AtpManager.get_prover prover_name (Proof.theory_of st))
val atp_timeout = AtpManager.get_timeout ()
val atp = prover atp_timeout NONE NONE prover_name 1
- val (success, (message, thm_names), _, _, _) =
+ val (success, (message, thm_names), time, _, _, _) =
TimeLimit.timeLimit timeout atp (Proof.get_goal st)
- in (success, message, SOME thm_names) end
- handle ResHolClause.TOO_TRIVIAL => (true, "trivial", SOME [])
- | TimeLimit.TimeOut => (false, "time out", NONE)
- | ERROR msg => (false, "error: " ^ msg, NONE)
+ in if success then (message, SOME (time, thm_names)) else (message, NONE) end
+ handle ResHolClause.TOO_TRIVIAL => ("trivial", SOME (0, []))
+ | TimeLimit.TimeOut => ("time out", NONE)
+ | ERROR msg => ("error: " ^ msg, NONE)
in
@@ -65,16 +62,20 @@
AList.lookup (op =) args proverK
|> the_default (hd (space_explode " " (AtpManager.get_atps ())))
val dir = AList.lookup (op =) args keepK
- val ((success, msg, thm_names), time) =
- safe init done (Mirabelle.cpu_time (run prover_name timeout st)) dir
- fun sh_log s = log ("sledgehammer: " ^ with_time success time ^ " [" ^
- prover_name ^ "]" ^ s)
- val _ = if success then sh_log (":\n" ^ msg) else sh_log ""
- in if success then thm_names else NONE end
+ val (msg, result) = safe init done (run prover_name timeout st) dir
+ val _ =
+ if is_some result
+ then log ("sledgehammer: succeeded (" ^ string_of_int (fst (the result)) ^
+ ") [" ^ prover_name ^ "]:\n" ^ msg)
+ else log ("sledgehammer: failed: " ^ msg)
+ in Option.map snd result end
end
+fun with_time true t = "succeeded (" ^ string_of_int t ^ ")"
+ | with_time false t = "failed (" ^ string_of_int t ^ ")"
+
fun run_metis (args, st, timeout, log) thm_names =
let
fun get_thms ctxt = maps (thms_of_name ctxt)
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Thu Sep 03 15:47:39 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Thu Sep 03 17:55:31 2009 +0200
@@ -24,7 +24,7 @@
type prover = int -> (thm * (string * int)) list option ->
(thm * (string * int)) list option -> string -> int ->
Proof.context * (thm list * thm) ->
- bool * (string * string list) * string * string vector * (thm * (string * int)) list
+ bool * (string * string list) * int * string * string vector * (thm * (string * int)) list
val add_prover: string -> prover -> theory -> theory
val print_provers: theory -> unit
val get_prover: string -> theory -> prover option
@@ -305,7 +305,7 @@
type prover = int -> (thm * (string * int)) list option ->
(thm * (string * int)) list option -> string -> int ->
Proof.context * (thm list * thm) ->
- bool * (string * string list) * string * string vector * (thm * (string * int)) list
+ bool * (string * string list) * int * string * string vector * (thm * (string * int)) list
fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
@@ -345,7 +345,7 @@
let
val _ = register birthtime deadtime (Thread.self (), desc)
val result =
- let val (success, (message, _), _, _, _) =
+ let val (success, (message, _), _, _, _, _) =
prover (get_timeout ()) NONE NONE name i (Proof.get_goal proof_state)
in (success, message) end
handle ResHolClause.TOO_TRIVIAL
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Thu Sep 03 15:47:39 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Thu Sep 03 17:55:31 2009 +0200
@@ -83,7 +83,7 @@
("# Cannot determine problem status within resource limit", Timeout),
("Error", Error)]
-fun produce_answer (success, message, result_string, thm_name_vec, filtered) =
+fun produce_answer (success, message, _, result_string, thm_name_vec, filtered) =
if success then
(Success (Vector.foldr op:: [] thm_name_vec, filtered), result_string)
else
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Thu Sep 03 15:47:39 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Thu Sep 03 17:55:31 2009 +0200
@@ -79,19 +79,29 @@
preparer goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy
(* write out problem file and call prover *)
- fun cmd_line probfile = space_implode " " ["exec", File.shell_path cmd,
- args, File.platform_path probfile]
+ fun cmd_line probfile = "TIMEFORMAT='%3U'; ((time " ^ space_implode " "
+ [File.shell_path cmd, args, File.platform_path probfile] ^ ") 2>&1)"
+ fun split_time s =
+ let
+ val split = String.tokens (fn c => str c = "\n")
+ val (proof, t) = s |> split |> split_last |> apfst cat_lines
+ val num = Scan.many1 Symbol.is_ascii_digit >> (fst o read_int)
+ val time = num --| Scan.$$ "." -- num >> (fn (a, b) => a * 1000 + b)
+ val as_time = the_default 0 o Scan.read Symbol.stopper time o explode
+ in (proof, as_time t) end
fun run_on probfile =
if File.exists cmd
- then writer probfile clauses |> pair (system_out (cmd_line probfile))
+ then
+ writer probfile clauses
+ |> pair (apfst split_time (system_out (cmd_line probfile)))
else error ("Bad executable: " ^ Path.implode cmd)
(* if problemfile has not been exported, delete problemfile; otherwise export proof, too *)
fun cleanup probfile = if destdir' = "" then File.rm probfile else ()
- fun export probfile ((proof, _), _) = if destdir' = "" then ()
+ fun export probfile (((proof, _), _), _) = if destdir' = "" then ()
else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof
- val ((proof, rc), conj_pos) = with_path cleanup export run_on
+ val (((proof, time), rc), conj_pos) = with_path cleanup export run_on
(prob_pathname subgoalno)
(* check for success and print out some information on failure *)
@@ -103,7 +113,7 @@
else apfst (fn s => "Try this command: " ^ s)
(produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoalno))
val _ = Output.debug (fn () => "Sledgehammer response (rc = " ^ string_of_int rc ^ "):\n" ^ proof)
- in (success, message, proof, thm_names, the_filtered_clauses) end;
+ in (success, message, time, proof, thm_names, the_filtered_clauses) end;