162 | from_lemmas ss = " from " ^ space_implode " " (Try.serial_commas "and" (map quote ss)) |
162 | from_lemmas ss = " from " ^ space_implode " " (Try.serial_commas "and" (map quote ss)) |
163 |
163 |
164 fun string_of_atp_failure MaybeUnprovable = "Problem maybe unprovable" |
164 fun string_of_atp_failure MaybeUnprovable = "Problem maybe unprovable" |
165 | string_of_atp_failure Unprovable = "Unprovable problem" |
165 | string_of_atp_failure Unprovable = "Unprovable problem" |
166 | string_of_atp_failure GaveUp = "Gave up" |
166 | string_of_atp_failure GaveUp = "Gave up" |
167 | string_of_atp_failure ProofMissing = |
167 | string_of_atp_failure ProofMissing = "Proof missing" |
168 "Claims the conjecture is a theorem but did not provide a proof" |
168 | string_of_atp_failure ProofIncomplete = "Proof incomplete" |
169 | string_of_atp_failure ProofIncomplete = |
169 | string_of_atp_failure ProofUnparsable = "Proof unparsable" |
170 "Claims the conjecture is a theorem but provided an incomplete proof" |
|
171 | string_of_atp_failure ProofUnparsable = |
|
172 "Claims the conjecture is a theorem but provided an unparsable proof" |
|
173 | string_of_atp_failure (UnsoundProof (false, ss)) = |
170 | string_of_atp_failure (UnsoundProof (false, ss)) = |
174 "Derived the lemma \"False\"" ^ from_lemmas ss ^ |
171 "Derived the lemma \"False\"" ^ from_lemmas ss ^ |
175 ", probably due to the use of an unsound type encoding" |
172 ", probably due to the use of an unsound type encoding" |
176 | string_of_atp_failure (UnsoundProof (true, ss)) = |
173 | string_of_atp_failure (UnsoundProof (true, ss)) = |
177 "Derived the lemma \"False\"" ^ from_lemmas ss ^ |
174 "Derived the lemma \"False\"" ^ from_lemmas ss ^ |
178 ", which could be due to a bug in Sledgehammer or to inconsistent axioms (including \"sorry\"s)" |
175 ", which could be due to a bug in Sledgehammer or to inconsistent axioms (including \"sorry\"s)" |
179 | string_of_atp_failure TimedOut = "Timed out" |
176 | string_of_atp_failure TimedOut = "Timed out" |
180 | string_of_atp_failure Inappropriate = "Problem outside the prover's scope" |
177 | string_of_atp_failure Inappropriate = "Problem outside the prover's scope" |
181 | string_of_atp_failure OutOfResources = "Ran out of resources" |
178 | string_of_atp_failure OutOfResources = "Out of resources" |
182 | string_of_atp_failure MalformedInput = "Malformed problem" |
179 | string_of_atp_failure MalformedInput = "Malformed problem" |
183 | string_of_atp_failure MalformedOutput = "Malformed output" |
180 | string_of_atp_failure MalformedOutput = "Malformed output" |
184 | string_of_atp_failure Interrupted = "Interrupted" |
181 | string_of_atp_failure Interrupted = "Interrupted" |
185 | string_of_atp_failure Crashed = "Crashed" |
182 | string_of_atp_failure Crashed = "Crashed" |
186 | string_of_atp_failure InternalError = "Internal prover error" |
183 | string_of_atp_failure InternalError = "Internal prover error" |