summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | blanchet |

Fri, 27 Aug 2021 14:29:02 +0200 | |

changeset 74207 | adf767b94f77 |

parent 74206 | 9c6159cbf9ee |

child 74208 | 1a8d8dd77513 |

handle Zipperposition's ResourceOut gracefully

src/HOL/Tools/ATP/atp_proof.ML | file | annotate | diff | comparison | revisions | |

src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Tools/ATP/atp_proof.ML Fri Aug 27 14:28:56 2021 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Fri Aug 27 14:29:02 2021 +0200 @@ -157,32 +157,31 @@ fun from_lemmas [] = "" | from_lemmas ss = " from " ^ space_implode " " (Try.serial_commas "and" (map quote ss)) -fun string_of_atp_failure MaybeUnprovable = "The generated problem is maybe unprovable" - | string_of_atp_failure Unprovable = "The generated problem is unprovable" - | string_of_atp_failure GaveUp = "The prover gave up" +fun string_of_atp_failure MaybeUnprovable = "Problem maybe unprovable" + | string_of_atp_failure Unprovable = "Unprovable problem" + | string_of_atp_failure GaveUp = "Gave up" | string_of_atp_failure ProofMissing = - "The prover claims the conjecture is a theorem but did not provide a proof" + "Claims the conjecture is a theorem but did not provide a proof" | string_of_atp_failure ProofIncomplete = - "The prover claims the conjecture is a theorem but provided an incomplete proof" + "Claims the conjecture is a theorem but provided an incomplete proof" | string_of_atp_failure ProofUnparsable = - "The prover claims the conjecture is a theorem but provided an unparsable proof" + "Claims the conjecture is a theorem but provided an unparsable proof" | string_of_atp_failure (UnsoundProof (false, ss)) = - "The prover derived the lemma \"False\"" ^ from_lemmas ss ^ - "; specify a sound type encoding or omit the \"type_enc\" option" + "Derived the lemma \"False\"" ^ from_lemmas ss ^ + ", probably due to the use of an unsound type encoding" | string_of_atp_failure (UnsoundProof (true, ss)) = - "The prover derived the lemma \"False\"" ^ from_lemmas ss ^ + "Derived the lemma \"False\"" ^ from_lemmas ss ^ ", which could be due to a bug in Sledgehammer or to inconsistent axioms (including \"sorry\"s)" | string_of_atp_failure TimedOut = "Timed out" - | string_of_atp_failure Inappropriate = - "The generated problem lies outside the prover's scope" - | string_of_atp_failure OutOfResources = "The prover ran out of resources" - | string_of_atp_failure MalformedInput = "The generated problem is malformed" - | string_of_atp_failure MalformedOutput = "The prover output is malformed" - | string_of_atp_failure Interrupted = "The prover was interrupted" - | string_of_atp_failure Crashed = "The prover crashed" - | string_of_atp_failure InternalError = "An internal prover error occurred" + | string_of_atp_failure Inappropriate = "Problem outside the prover's scope" + | string_of_atp_failure OutOfResources = "Ran out of resources" + | string_of_atp_failure MalformedInput = "Malformed problem" + | string_of_atp_failure MalformedOutput = "Malformed output" + | string_of_atp_failure Interrupted = "Interrupted" + | string_of_atp_failure Crashed = "Crashed" + | string_of_atp_failure InternalError = "Internal prover error" | string_of_atp_failure (UnknownError s) = - "A prover error occurred" ^ + "Prover error" ^ (if s = "" then " (pass the \"verbose\" option for details)" else ":\n" ^ s) fun extract_delimited (begin_delim, end_delim) output =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Fri Aug 27 14:28:56 2021 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Fri Aug 27 14:29:02 2021 +0200 @@ -557,7 +557,9 @@ ["--input tptp --output tptp --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem |> extra_options <> "" ? prefix (extra_options ^ " ")], proof_delims = tstp_proof_delims, - known_failures = known_szs_status_failures, + known_failures = + [(TimedOut, "SZS status ResourceOut")] @ (* odd way of timing out *) + known_szs_status_failures, prem_role = Hypothesis, best_slices = fn _ => (* FUDGE *)