The Coq mailing list

[AUGER <Cedric.Auger AT lri.fr>]

Le Sun, 14 Mar 2010 17:01:12 +0100, Robin Green <greenrd AT greenrd.org> a  
écrit:

> In my years of using Coq I've encountered many different error
> messages which are "unsatisfactory", either because:
>
> (1) they refer to variables created by a tactic which eventually
> failed, so I have no idea what the error message is referring to
>
> or (2) they are hard to understand because they are hard to relate back
> to the original tactic invocation made by me
>
> or (3) a tactic seems to be failing to do a simple thing which it ought
> to be able to do, and which ought to be within its remit, judging by
> its documentation
>
> However, I don't generally report these to the bug database. I
> typically only report error messages which say "please report". Partly
> this is for time reasons, but partly because I am unsure how such
> reports would be received, and whether submitting them would be
> worthwhile.

I think that if you encounter strange errors you should ask in the mailing  
list, then posting.
Lot of things seem bugs, but somebody often explains you why it isn't.

> Should these types of error messages be reported to the bug database?
> And if so, should they be reported as bugs, as opposed to requests for
> enhancement?
>
> I hope so, because fixing these issues could improve the usability of
> Coq. And if some tactics fail for incomprehensible reasons, people
> might stop using them altogether, and then come away with the false
> impression that proving something serious in Coq takes too long.

I admit, that often errors are not very clear. For them you can ask to  
send better error messages in the bug tracking system

> On the other hand, (3) can be debatable in some cases, because you
> might be looking at a specific decidable case of a problem which is
> undecidable in general.
>
> I have a good example of case (3) right now. I had something like:
>
> H : foo F G x ~= foo F G y
>
> and did "injection H". It failed with an error message like:
>
> Toplevel input, characters 46-59:
> Error: Impossible to unify "foo F G x ~= foo F G y" with
>
>  "{n : nat &
>   {A : Type &
>   {B : Type &
>     (* ... details omitted by me for clarity *)
>   ~=
>   foo F G y".
>
> which makes me think "What?! Why on earth is it trying to do that? foo
> doesn't even yield something in a sig type - it's a constructor of
> some other type! That's obviously bogus!" So this is actually a case
> of (2) as well.

Do you use Coercion? If so, it may be normal.
Same thing if you redefined the injection tactic.

> However, if I merely apply JMeq_eq in H and then do the injection, it
> succeeds. So this is a case of (3): in my opinion, it ought to be able
> to do what I did (apply JMeq_eq first, then proceed as normal).
>
> (Note that I have patched the injection tactic to fix bug 2255, so
> this particular issue could be a bug that only occurs in my patched
> version of Coq. But this is just an example to show what I mean by (3)
> above.)

Have you tried to use an not patched version?


--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay