The Coq mailing list

[Robin Green <greenrd AT greenrd.org>]

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.

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.

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.

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

-- 
Robin