# HG changeset patch # User blanchet # Date 1272030514 -7200 # Node ID a4f601daa17516e8b373e6d0471c46233349508a # Parent d2cd0d04b8e6334612cd5a376c016fcf2c51fce8 centralized ATP-specific error handling in "atp_wrapper.ML" diff -r d2cd0d04b8e6 -r a4f601daa175 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Apr 23 13:16:50 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Apr 23 15:48:34 2010 +0200 @@ -34,8 +34,11 @@ relevance_override: relevance_override, axiom_clauses: (thm * (string * int)) list option, filtered_clauses: (thm * (string * int)) list option} + datatype failure = + Unprovable | TimedOut | OutOfResources | OldSpass | MalformedOutput | + UnknownError type prover_result = - {success: bool, + {outcome: failure option, message: string, relevant_thm_names: string list, atp_run_time_in_msecs: int, @@ -95,8 +98,12 @@ axiom_clauses: (thm * (string * int)) list option, filtered_clauses: (thm * (string * int)) list option}; +datatype failure = + Unprovable | TimedOut | OutOfResources | OldSpass | MalformedOutput | + UnknownError + type prover_result = - {success: bool, + {outcome: failure option, message: string, relevant_thm_names: string list, atp_run_time_in_msecs: int, @@ -248,7 +255,7 @@ do (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action |> these - |> List.app (unregister params "Timed out."); + |> List.app (unregister params "Timed out.\n"); print_new_messages (); (*give threads some time to respond to interrupt*) OS.Process.sleep min_wait_time) diff -r d2cd0d04b8e6 -r a4f601daa175 src/HOL/Tools/ATP_Manager/atp_minimal.ML --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Apr 23 13:16:50 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Apr 23 15:48:34 2010 +0200 @@ -1,5 +1,6 @@ (* Title: HOL/Tools/ATP_Manager/atp_minimal.ML Author: Philipp Meyer, TU Muenchen + Author: Jasmin Blanchette, TU Muenchen Minimization of theorem list for Metis using automatic theorem provers. *) @@ -35,34 +36,16 @@ in aux s end -(* failure check and producing answer *) - -datatype outcome = Success | Failure | Timeout | Error - -val string_of_outcome = - fn Success => "Success" - | Failure => "Failure" - | Timeout => "Timeout" - | Error => "Error" +(* wrapper for calling external prover *) -(* FIXME: move to "atp_wrapper.ML" *) -val failure_strings = - [("SPASS beiseite: Ran out of time.", Timeout), - ("Timeout", Timeout), - ("time limit exceeded", Timeout), - ("# Cannot determine problem status within resource limit", Timeout), - ("Error", Error)] - -fun outcome_of_result (result as {success, output, ...} : prover_result) = - if success then - Success - else case get_first (fn (s, outcome) => - if String.isSubstring s output then SOME outcome - else NONE) failure_strings of - SOME outcome => outcome - | NONE => Failure - -(* wrapper for calling external prover *) +fun string_for_failure Unprovable = "Unprovable." + | string_for_failure TimedOut = "Timed out." + | string_for_failure OutOfResources = "Failed." + | string_for_failure OldSpass = "Error." + | string_for_failure MalformedOutput = "Error." + | string_for_failure UnknownError = "Failed." +fun string_for_outcome NONE = "Success." + | string_for_outcome (SOME failure) = string_for_failure failure fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover timeout subgoal state filtered_clauses name_thms_pairs = @@ -79,8 +62,8 @@ axiom_clauses = SOME axclauses, filtered_clauses = SOME (the_default axclauses filtered_clauses)} in - `outcome_of_result (prover params (K "") timeout problem) - |>> tap (priority o string_of_outcome) + prover params (K "") timeout problem + |> tap (priority o string_for_outcome o #outcome) end (* minimalization of thms *) @@ -98,7 +81,7 @@ sledgehammer_test_theorems params prover minimize_timeout i state fun test_thms filtered thms = case test_thms_fun filtered thms of - (Success, result) => SOME result + (result as {outcome = NONE, ...}) => SOME result | _ => NONE val {context = ctxt, facts, goal} = Proof.goal state; @@ -106,7 +89,7 @@ in (* try prove first to check result and get used theorems *) (case test_thms_fun NONE name_thms_pairs of - (Success, result as {internal_thm_names, filtered_clauses, ...}) => + result as {outcome = NONE, internal_thm_names, filtered_clauses, ...} => let val used = internal_thm_names |> Vector.foldr (op ::) [] |> sort_distinct string_ord @@ -126,17 +109,17 @@ proof_text isar_proof debug modulus sorts ctxt (K "", proof, internal_thm_names, goal, i) |> fst) end - | (Timeout, _) => + | {outcome = SOME TimedOut, ...} => (NONE, "Timeout: You can increase the time limit using the \"timeout\" \ \option (e.g., \"timeout = " ^ string_of_int (10 + msecs div 1000) ^ " s\").") - | (Error, {message, ...}) => (NONE, "ATP error: " ^ message) - | (Failure, _) => + | {outcome = SOME UnknownError, ...} => (* Failure sometimes mean timeout, unfortunately. *) (NONE, "Failure: No proof was found with the current time limit. You \ \can increase the time limit using the \"timeout\" \ \option (e.g., \"timeout = " ^ - string_of_int (10 + msecs div 1000) ^ " s\").")) + string_of_int (10 + msecs div 1000) ^ " s\").") + | {message, ...} => (NONE, "ATP error: " ^ message)) handle Sledgehammer_HOL_Clause.TRIVIAL => (SOME [], metis_line i n []) | ERROR msg => (NONE, "Error: " ^ msg) diff -r d2cd0d04b8e6 -r a4f601daa175 src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Apr 23 13:16:50 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Apr 23 15:48:34 2010 +0200 @@ -43,20 +43,20 @@ (* prover configuration *) -val remotify = prefix "remote_" - type prover_config = - {home: string, - executable: string, - arguments: Time.time -> string, - proof_delims: (string * string) list, - known_failures: (string list * string) list, - max_new_clauses: int, - prefers_theory_relevant: bool}; + {home: string, + executable: string, + arguments: Time.time -> string, + proof_delims: (string * string) list, + known_failures: (failure * string) list, + max_new_clauses: int, + prefers_theory_relevant: bool}; (* basic template *) +val remotify = prefix "remote_" + fun with_path cleanup after f path = Exn.capture f path |> tap (fn _ => cleanup path) @@ -72,17 +72,30 @@ |> first_field end_delim |> the |> fst | _ => "" -fun extract_proof_or_failure proof_delims known_failures output = - case map_filter - (fn (patterns, message) => - if exists (fn p => String.isSubstring p output) patterns then - SOME message - else - NONE) known_failures of +fun extract_proof_and_outcome res_code proof_delims known_failures output = + case map_filter (fn (failure, pattern) => + if String.isSubstring pattern output then SOME failure + else NONE) known_failures of [] => (case extract_proof proof_delims output of - "" => ("", "Error: The ATP output is malformed.") - | proof => (proof, "")) - | (message :: _) => ("", message) + "" => ("", SOME UnknownError) + | proof => if res_code = 0 then (proof, NONE) + else ("", SOME UnknownError)) + | (failure :: _) => ("", SOME failure) + +fun string_for_failure Unprovable = "The ATP problem is unprovable." + | string_for_failure TimedOut = "Timed out." + | string_for_failure OutOfResources = "The ATP ran out of resources." + | string_for_failure OldSpass = + "Warning: Sledgehammer requires a more recent version of SPASS with \ + \support for the TPTP syntax. To install it, download and untar the \ + \package \"http://isabelle.in.tum.de/~blanchet/spass-3.7.tgz\" and add the \ + \\"spass-3.7\" directory's full path to \"" ^ + Path.implode (Path.expand (Path.appends + (Path.variable "ISABELLE_HOME_USER" :: + map Path.basic ["etc", "components"]))) ^ + "\" on a line of its own." + | string_for_failure MalformedOutput = "Error: The ATP output is malformed." + | string_for_failure UnknownError = "Error: An unknown ATP error occurred." fun generic_prover overlord get_facts prepare write_file home executable args proof_delims known_failures name @@ -176,23 +189,20 @@ else "") ^ output) - val (((output, atp_run_time_in_msecs), rc), _) = + val (((output, atp_run_time_in_msecs), res_code), _) = with_path cleanup export run_on (prob_pathname subgoal); (* Check for success and print out some information on failure. *) - val (proof, failure) = - extract_proof_or_failure proof_delims known_failures output - val success = (rc = 0 andalso failure = "") + val (proof, outcome) = + extract_proof_and_outcome res_code proof_delims known_failures output val (message, relevant_thm_names) = - if success then - proof_text isar_proof debug modulus sorts ctxt - (minimize_command, proof, internal_thm_names, th, subgoal) - else if failure <> "" then - (failure ^ "\n", []) - else - ("Unknown ATP error: " ^ output ^ ".\n", []) + case outcome of + NONE => proof_text isar_proof debug modulus sorts ctxt + (minimize_command, proof, internal_thm_names, th, + subgoal) + | SOME failure => (string_for_failure failure ^ "\n", []) in - {success = success, message = message, + {outcome = outcome, message = message, relevant_thm_names = relevant_thm_names, atp_run_time_in_msecs = atp_run_time_in_msecs, output = output, proof = proof, internal_thm_names = internal_thm_names, @@ -237,10 +247,9 @@ proof_delims = [("=========== Refutation ==========", "======= End of refutation =======")], known_failures = - [(["Satisfiability detected", "CANNOT PROVE"], - "The ATP problem is unprovable."), - (["Refutation not found"], - "The ATP failed to determine the problem's status.")], + [(Unprovable, "Satisfiability detected"), + (OutOfResources, "CANNOT PROVE"), + (OutOfResources, "Refutation not found")], max_new_clauses = 60, prefers_theory_relevant = false} val vampire = tptp_prover "vampire" vampire_config @@ -259,12 +268,14 @@ string_of_int (generous_to_secs timeout)), proof_delims = [tstp_proof_delims], known_failures = - [(["SZS status: Satisfiable", "SZS status Satisfiable"], - "The ATP problem is unprovable."), - (["SZS status: ResourceOut", "SZS status ResourceOut"], - "The ATP ran out of resources."), - (["# Cannot determine problem status"], - "The ATP failed to determine the problem's status.")], + [(Unprovable, "SZS status: Satisfiable"), + (Unprovable, "SZS status Satisfiable"), + (TimedOut, "Failure: Resource limit exceeded (time)"), + (TimedOut, "time limit exceeded"), + (OutOfResources, + "# Cannot determine problem status within resource limit"), + (OutOfResources, "SZS status: ResourceOut"), + (OutOfResources, "SZS status ResourceOut")], max_new_clauses = 100, prefers_theory_relevant = false} val e = tptp_prover "e" e_config @@ -298,10 +309,9 @@ string_of_int (generous_to_secs timeout)), proof_delims = [("Here is a proof", "Formulae used in the proof")], known_failures = - [(["SPASS beiseite: Completion found."], "The ATP problem is unprovable."), - (["SPASS beiseite: Ran out of time."], "The ATP timed out."), - (["SPASS beiseite: Maximal number of loops exceeded."], - "The ATP hit its loop limit.")], + [(Unprovable, "SPASS beiseite: Completion found"), + (TimedOut, "SPASS beiseite: Ran out of time"), + (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded")], max_new_clauses = 40, prefers_theory_relevant = true} val spass = dfg_prover "spass" spass_config @@ -321,15 +331,8 @@ proof_delims = #proof_delims spass_config, known_failures = #known_failures spass_config @ - [(["unrecognized option `-TPTP'", "Unrecognized option TPTP"], - "Warning: Sledgehammer requires a more recent version of SPASS with \ - \support for the TPTP syntax. To install it, download and untar the \ - \package \"http://isabelle.in.tum.de/~blanchet/spass-3.7.tgz\" and add \ - \the \"spass-3.7\" directory's full path to \"" ^ - Path.implode (Path.expand (Path.appends - (Path.variable "ISABELLE_HOME_USER" :: - map Path.basic ["etc", "components"]))) ^ - "\" on a line of its own.")], + [(OldSpass, "unrecognized option `-TPTP'"), + (OldSpass, "Unrecognized option TPTP")], max_new_clauses = #max_new_clauses spass_config, prefers_theory_relevant = #prefers_theory_relevant spass_config} val spass_tptp = tptp_prover "spass_tptp" spass_tptp_config @@ -339,14 +342,10 @@ val systems = Synchronized.var "atp_wrapper_systems" ([]: string list); fun get_systems () = - let - val (answer, rc) = bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w" - in - if rc <> 0 then - error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer) - else - split_lines answer - end; + case bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w" of + (answer, 0) => split_lines answer + | (answer, _) => + error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer) fun refresh_systems_on_tptp () = Synchronized.change systems (fn _ => get_systems ()); @@ -357,12 +356,13 @@ fun the_system prefix = (case get_system prefix of - NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP") + NONE => error ("System " ^ quote prefix ^ + " not available at SystemOnTPTP.") | SOME sys => sys); val remote_known_failures = - [(["Remote-script could not extract proof"], - "Error: The remote ATP proof is ill-formed.")] + [(TimedOut, "says Timeout"), + (MalformedOutput, "Remote-script could not extract proof")] fun remote_prover_config prover_prefix args ({proof_delims, known_failures, max_new_clauses,