Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] type-unsound error


view this post on Zulip Email Gateway (Aug 19 2022 at 12:15):

From: marco caminati <marco.caminati@yahoo.it>
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.

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?

Thanks,
Marco
PS: possible double post for technical problems, sorry

"remote_e_sine": The prover found a type-unsound proof involving "Domain_converse", "Domain_empty", "Image_empty", "Image_within_domain", "Int_empty_left", "Int_empty_right", "Range_empty", "Set.is_empty_def", "empty_Collect_eq", "empty_iff", "equals0D", "ll1", "ll67", and "mem_Collect_eq" even though a supposedly type-sound encoding was used (or, less likely, your axioms are inconsistent). Please report this to the Isabelle developers.

view this post on Zulip Email Gateway (Aug 19 2022 at 12:17):

From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Marco,

Am 04.10.2013 um 08:47 schrieb marco caminati <marco.caminati@yahoo.it>:

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.

Regards,

Jasmin

view this post on Zulip Email Gateway (Aug 19 2022 at 12:17):

From: marco caminati <marco.caminati@yahoo.it>
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.

Thanks,
Marco


Last updated: Mar 29 2024 at 01:04 UTC