Re: [isabelle] type-unsound error

Il ven 4 ott 2013 10:53 CEST, Jasmin Blanchette ha scritto:

>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. 

...and this turned out to be the case, too. Sorry about my unprovable sorries.

>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.

Definitely more helpful. This thread, too, could be of future reference.


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