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

author | blanchet |

Wed, 28 Aug 2013 18:44:50 +0200 | |

changeset 53224 | f13c49dd9805 |

parent 53223 | 79e5b668f716 |

child 53225 | 16235bb41881 |

tuned messages

src/Doc/Sledgehammer/document/root.tex | file | annotate | diff | comparison | revisions | |

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

--- a/src/Doc/Sledgehammer/document/root.tex Wed Aug 28 18:44:50 2013 +0200 +++ b/src/Doc/Sledgehammer/document/root.tex Wed Aug 28 18:44:50 2013 +0200 @@ -601,14 +601,15 @@ \point{A strange error occurred---what should I do?} Sledgehammer tries to give informative error messages. Please report any strange -error to the author at \authoremail. This applies double if you get the message +error to the author at \authoremail. This applies doubly if you get the message \prew \slshape -The prover found a type-unsound proof involving ``\textit{foo\/}'', -``\textit{bar\/}'', and ``\textit{baz\/}'' even though a supposedly type-sound -encoding was used (or, less likely, your axioms are inconsistent). You might -want to report this to the Isabelle developers. +The prover derived ``\textit{False}'' using ``\textit{foo\/}'', +``\textit{bar\/}'', and ``\textit{baz\/}''. +This could be due to inconsistent axioms (including ``\textbf{sorry}''s) or to +a bug in Sledgehammer. If the problem persists, please contact the +Isabelle developers. \postw \point{Auto can solve it---why not Sledgehammer?}

--- a/src/HOL/Tools/ATP/atp_proof.ML Wed Aug 28 18:44:50 2013 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Aug 28 18:44:50 2013 +0200 @@ -103,8 +103,7 @@ fun involving [] = "" | involving ss = - "involving " ^ space_implode " " (Try.serial_commas "and" (map quote ss)) ^ - " " + " involving " ^ space_implode " " (Try.serial_commas "and" (map quote ss)) fun string_of_failure Unprovable = "The generated problem is unprovable." | string_of_failure GaveUp = "The prover gave up." @@ -114,13 +113,13 @@ "The prover claims the conjecture is a theorem but provided an incomplete \ \(or unparsable) proof." | string_of_failure (UnsoundProof (false, ss)) = - "The prover found an unsound proof " ^ involving ss ^ - "(or, less likely, your axioms are inconsistent). Specify a sound type \ - \encoding or omit the \"type_enc\" option." + "The prover derived \"False\" using" ^ involving ss ^ + ". Specify a sound type encoding or omit the \"type_enc\" option." | string_of_failure (UnsoundProof (true, ss)) = - "The prover found an unsound proof " ^ involving ss ^ - "(or, less likely, your axioms are inconsistent). Please report this to \ - \the Isabelle developers." + "The prover derived \"False\" using" ^ involving ss ^ + ". This could be due to inconsistent axioms (including \"sorry\"s) or to \ + \a bug in Sledgehammer. If the problem persists, please contact the \ + \Isabelle developers." | string_of_failure CantConnect = "Cannot connect to remote server." | string_of_failure TimedOut = "Timed out." | string_of_failure Inappropriate =