# HG changeset patch # User blanchet # Date 1271851354 -7200 # Node ID 26fb60d9d3f205ef832b53adcf2fd1cf3eb27d04 # Parent d7d1d87276b753e872480ec8b4e9d1df36a3271e# Parent 28188e3650ee23a08b1d14e3be016465767b946d merged diff -r d7d1d87276b7 -r 26fb60d9d3f2 src/HOL/Tools/ATP_Manager/atp_minimal.ML --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Wed Apr 21 12:11:48 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Wed Apr 21 14:02:34 2010 +0200 @@ -71,7 +71,7 @@ " theorem" ^ plural_s num_theorems ^ "...") val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs - val {context = ctxt, facts, goal} = Proof.raw_goal state + val {context = ctxt, facts, goal} = Proof.goal state val problem = {subgoal = subgoal, goal = (ctxt, (facts, goal)), relevance_override = {add = [], del = [], only = false}, diff -r d7d1d87276b7 -r 26fb60d9d3f2 src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Wed Apr 21 12:11:48 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Wed Apr 21 14:02:34 2010 +0200 @@ -46,7 +46,7 @@ type prover_config = {command: Path.T, arguments: Time.time -> string, - failure_strs: string list, + known_failures: (string list * string) list, max_new_clauses: int, prefers_theory_relevant: bool, supports_isar_proofs: bool}; @@ -60,13 +60,18 @@ |> Exn.release |> tap (after path); -fun find_failure strs proof = - case filter (fn s => String.isSubstring s proof) strs of - [] => if is_proof_well_formed proof then NONE - else SOME "Ill-formed ATP output" - | (failure :: _) => SOME failure +fun find_known_failure known_failures proof = + case map_filter (fn (patterns, message) => + if exists (fn pattern => String.isSubstring pattern proof) + patterns then + SOME message + else + NONE) known_failures of + [] => if is_proof_well_formed proof then "" + else "Error: The ATP output is ill-formed." + | (message :: _) => message -fun generic_prover overlord get_facts prepare write_file cmd args failure_strs +fun generic_prover overlord get_facts prepare write_file cmd args known_failures proof_text name ({debug, full_types, explicit_apply, ...} : params) ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses} : problem) = @@ -106,13 +111,12 @@ (* write out problem file and call prover *) fun cmd_line probfile = - if Config.get ctxt measure_runtime - then (* Warning: suppresses error messages of ATPs *) + if Config.get ctxt measure_runtime then "TIMEFORMAT='%3U'; { time " ^ space_implode " " [File.shell_path cmd, - args, File.shell_path probfile] ^ " 2> /dev/null" ^ " ; } 2>&1" + args, File.shell_path probfile] ^ " ; } 2>&1" else space_implode " " ["exec", File.shell_path cmd, args, - File.shell_path probfile]; + File.shell_path probfile, "2>&1"]; fun split_time s = let val split = String.tokens (fn c => str c = "\n"); @@ -146,12 +150,15 @@ with_path cleanup export run_on (prob_pathname subgoal); (* Check for success and print out some information on failure. *) - val failure = find_failure failure_strs proof; - val success = rc = 0 andalso is_none failure; + val failure = find_known_failure known_failures proof; + val success = rc = 0 andalso failure = ""; val (message, relevant_thm_names) = - if is_some failure then ("ATP failed to find a proof.\n", []) - else if rc <> 0 then ("ATP error: " ^ proof ^ ".\n", []) - else proof_text name proof internal_thm_names ctxt th subgoal + if success then + proof_text name proof internal_thm_names ctxt th subgoal + else if failure <> "" then + (failure, []) + else + ("Unknown ATP error: " ^ proof ^ ".\n", []) in {success = success, message = message, relevant_thm_names = relevant_thm_names, @@ -164,19 +171,19 @@ (* generic TPTP-based provers *) fun generic_tptp_prover - (name, {command, arguments, failure_strs, max_new_clauses, + (name, {command, arguments, known_failures, max_new_clauses, prefers_theory_relevant, supports_isar_proofs}) - (params as {overlord, respect_no_atp, relevance_threshold, convergence, - theory_relevant, higher_order, follow_defs, isar_proof, - modulus, sorts, ...}) + (params as {debug, overlord, respect_no_atp, relevance_threshold, + convergence, theory_relevant, higher_order, follow_defs, + isar_proof, modulus, sorts, ...}) timeout = generic_prover overlord (get_relevant_facts respect_no_atp relevance_threshold convergence higher_order follow_defs max_new_clauses (the_default prefers_theory_relevant theory_relevant)) (prepare_clauses higher_order false) - (write_tptp_file (overlord andalso not isar_proof)) command - (arguments timeout) failure_strs + (write_tptp_file (debug andalso overlord andalso not isar_proof)) command + (arguments timeout) known_failures (proof_text (supports_isar_proofs andalso isar_proof) false modulus sorts) name params @@ -195,8 +202,11 @@ {command = Path.explode "$VAMPIRE_HOME/vampire", arguments = (fn timeout => "--output_syntax tptp --mode casc -t " ^ string_of_int (generous_to_secs timeout)), - failure_strs = - ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"], + known_failures = + [(["Satisfiability detected", "CANNOT PROVE"], + "The ATP problem is unprovable."), + (["Refutation not found"], + "The ATP failed to determine the problem's status.")], max_new_clauses = 60, prefers_theory_relevant = false, supports_isar_proofs = true} @@ -210,10 +220,13 @@ arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev \ \-tAutoDev --silent --cpu-limit=" ^ string_of_int (generous_to_secs timeout)), - failure_strs = - ["SZS status: Satisfiable", "SZS status Satisfiable", - "SZS status: ResourceOut", "SZS status ResourceOut", - "# Cannot determine problem status"], + 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.")], max_new_clauses = 100, prefers_theory_relevant = false, supports_isar_proofs = true} @@ -223,7 +236,7 @@ (* SPASS *) fun generic_dfg_prover - (name, ({command, arguments, failure_strs, max_new_clauses, + (name, ({command, arguments, known_failures, max_new_clauses, prefers_theory_relevant, ...} : prover_config)) (params as {overlord, respect_no_atp, relevance_threshold, convergence, theory_relevant, higher_order, follow_defs, ...}) @@ -233,10 +246,10 @@ higher_order follow_defs max_new_clauses (the_default prefers_theory_relevant theory_relevant)) (prepare_clauses higher_order true) write_dfg_file command - (arguments timeout) failure_strs (metis_proof_text false false) + (arguments timeout) known_failures (metis_proof_text false false) name params -fun dfg_prover (name, p) = (name, generic_dfg_prover (name, p)); +fun dfg_prover name p = (name, generic_dfg_prover (name, p)) (* The "-VarWeight=3" option helps the higher-order problems, probably by counteracting the presence of "hAPP". *) @@ -245,14 +258,42 @@ arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^ " -FullRed=0 -DocProof -VarWeight=3 -TimeLimit=" ^ string_of_int (generous_to_secs timeout)), - failure_strs = - ["SPASS beiseite: Completion found.", "SPASS beiseite: Ran out of time.", - "SPASS beiseite: Maximal number of loops exceeded."], + 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.")], max_new_clauses = 40, prefers_theory_relevant = true, supports_isar_proofs = false} -val spass = dfg_prover ("spass", spass_config) +val spass = dfg_prover "spass" spass_config + +(* SPASS 3.7 supports both the DFG and the TPTP syntax, whereas SPASS 3.0 + supports only the DFG syntax. As soon as all Isabelle repository/snapshot + users have upgraded to 3.7, we can kill "spass" (and all DFG support in + Sledgehammer) and rename "spass_tptp" "spass". *) + +(* FIXME: Change the error message below to point to the Isabelle download + page once the package is there (around the Isabelle2010 release). *) +val spass_tptp_config = + {command = #command spass_config, + arguments = prefix "-TPTP " o #arguments 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.")], + max_new_clauses = #max_new_clauses spass_config, + prefers_theory_relevant = #prefers_theory_relevant spass_config, + supports_isar_proofs = #supports_isar_proofs spass_config} +val spass_tptp = tptp_prover "spass_tptp" spass_tptp_config (* remote prover invocation via SystemOnTPTP *) @@ -280,16 +321,18 @@ NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP") | SOME sys => sys); -val remote_failure_strs = ["Remote-script could not extract proof"]; +val remote_known_failures = + [(["Remote-script could not extract proof"], + "Error: The remote ATP proof is ill-formed.")] fun remote_prover_config prover_prefix args - ({failure_strs, max_new_clauses, prefers_theory_relevant, ...} + ({known_failures, max_new_clauses, prefers_theory_relevant, ...} : prover_config) : prover_config = {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP", arguments = (fn timeout => args ^ " -t " ^ string_of_int (generous_to_secs timeout) ^ " -s " ^ the_system prover_prefix), - failure_strs = remote_failure_strs @ failure_strs, + known_failures = remote_known_failures @ known_failures, max_new_clauses = max_new_clauses, prefers_theory_relevant = prefers_theory_relevant, supports_isar_proofs = false} @@ -304,7 +347,8 @@ val remote_spass = tptp_prover "remote_spass" (remote_prover_config "SPASS---" "-x" spass_config) -val provers = [spass, vampire, e, remote_vampire, remote_spass, remote_e] +val provers = [spass, spass_tptp, vampire, e, remote_vampire, remote_spass, + remote_e] val prover_setup = fold add_prover provers val setup = diff -r d7d1d87276b7 -r 26fb60d9d3f2 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Apr 21 12:11:48 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Apr 21 14:02:34 2010 +0200 @@ -162,7 +162,7 @@ \directory's full path to \"" ^ Path.implode (Path.expand (Path.appends (Path.variable "ISABELLE_HOME_USER" :: - map Path.basic ["etc", "components"]))) ^ "\"." + map Path.basic ["etc", "components"]))) ^ "\" on a line of its own." val max_unsound_delay_ms = 200 val max_unsound_delay_percent = 2