# HG changeset patch # User haftmann # Date 1252002367 -7200 # Node ID 34c5e5b343029b97463291757d747a00cc3788aa # Parent 43d2ac4aa2de8e73df4529a2a86023559ea192c8# Parent 94f61caa546e2020d71b87a4e66291cffdc58fec merged diff -r 94f61caa546e -r 34c5e5b34302 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Sep 03 17:26:10 2009 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Sep 03 20:26:07 2009 +0200 @@ -25,12 +25,10 @@ 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" +val full_typesK = "full_types" local @@ -50,12 +48,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 +63,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) @@ -101,7 +103,9 @@ run_sledgehammer (args, pre, timeout, log) |> run_metis (args, pre, timeout, log) -fun invoke args = Mirabelle.register ("sledgehammer", sledgehammer_action args) +fun invoke args = + let val _ = AtpManager.set_full_types (AList.defined (op =) args full_typesK) + in Mirabelle.register ("sledgehammer", sledgehammer_action args) end end diff -r 94f61caa546e -r 34c5e5b34302 src/HOL/Mirabelle/doc/options.txt --- a/src/HOL/Mirabelle/doc/options.txt Thu Sep 03 17:26:10 2009 +0200 +++ b/src/HOL/Mirabelle/doc/options.txt Thu Sep 03 20:26:07 2009 +0200 @@ -4,3 +4,4 @@ * keep=PATH: path where to keep temporary files created by sledgehammer * metis=X: apply metis with the theorems found by sledgehammer (X may be any non-empty string) + * full_types=X: turn on full-typed encoding (X may be any non-empty string) diff -r 94f61caa546e -r 34c5e5b34302 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Thu Sep 03 17:26:10 2009 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Thu Sep 03 20:26:07 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 diff -r 94f61caa546e -r 34c5e5b34302 src/HOL/Tools/ATP_Manager/atp_minimal.ML --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Thu Sep 03 17:26:10 2009 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Thu Sep 03 20:26:07 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 diff -r 94f61caa546e -r 34c5e5b34302 src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Thu Sep 03 17:26:10 2009 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Thu Sep 03 20:26:07 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;