Re: [isabelle] type-unsound error

Hi Marco,

Am 04.10.2013 um 08:47 schrieb marco caminati <marco.caminati at>:

> The full text of the sledgehammer error I got is appended here.
> Two questions:
> 1) This error depends on some sorried proofs before it: does this make it uninteresting, or should I submit it anyway? In the first case I will try to complete those proofs (I am positive, though not sure, they can be completed) and see if the error goes away; in the latter case I can save such work.

A few years ago, as Sledgehammer's translation code was evolving rapidly, this message usually indicated a bug in Sledgehammer. These days, the last N times that people have reported this error to me, it was because of a "sorry" that turned out to be unprovable. Hence I would suggest that you look more closely into your "sorry"s first. If the problem still arises then, I would be extremely interesting in getting a self-contained example (if possible) or otherwise get more information from you.

Incidentally, the message in Isabelle2013-1-RC should be slightly more helpful:

    The prover derived "False" using foo, bar, and baz.
    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.

> 2) The error message says to report to Isabelle developers, while the official sledgehammer reference explicitly mentions this particular error and says to report to its maintainer:if I do (see 1), whom should I report to?

The maintainer (= I) is one of the Isabelle developers, so there's no contradiction here. I didn't want to hard-code my email address in Isabelle, but I felt more comfortable to do so in a manual of which I am the author. Whether you send future bug reports directly to me or to the mailing list is up to you. The mailing list has the advantage that other people might jump in if I'm on vacation.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.