Hello, a beginner question here: I have the following mwe based loosely on the content here. The first definition is fine, but the second gives the error Not a truly recursive fixpoint. [non-recursive,fixpoints]coqtop
. Why does it do this, and how can I correct my definition to get a length function?
Open Scope list_scope.
Section MySection.
Variables A : Type.
Fixpoint myrepeat (n count : nat) : list nat :=
match count with
| O => nil
| S count' => n :: (myrepeat n count')
end.
Fixpoint mylength (l:list A) : nat :=
match l with
| nil => O
| h :: t => S (length t)
end.
End MySection.
Coq is telling you that mylength is not recursive. That’s because it calls length, while maybe you wanted to call mylength?
Perhaps we could give a more informative warning that suggests some possible arguments you probably wanted to give.
Something like: Expected "mylength" in "_ :: _" branch to be recursive
or something
Sometimes the warning is raised in situations where students use Fixpoint
when they should have used Definition
. So maybe the warning should suggest the two options: "If you did not intend to write a recursive definition, then use Definition
instead. If you intended to write a recursive definition, then maybe you are missing a recursive call."
Has there ever been any discussion on how helpful error messages should try to be? Ali and I tried to write a very descriptive error message for Print Notation
and at some point it was basically repeating the refman and super long, so we ended up removing many of the prompts we had added (although it still includes some).
I notice that most error messages in Coq don't do this kind of thing, but is it a design decision or simply something to be improved?
There's a lot of room for improvement in Coq error messages.
I don't think this is a design choice. IMHO we should eventually aim at much better error messages, even if that makes them super long, but it will take a long time to improve all the existing ones.
I'd assume current errors are not good because it's very hard to write good ones; but overly long messages can also be bad.
And an error message is an bad medium to give the user a course about a feature — a tutorial is a better place.
e.g., https://twitter.com/b0rk/status/954366146505052160/photo/1 does _not_ teach the user what a comparison or a generic argument is — because their teaching material does that.
another great Rust compiler error message! (this is a parsing error which makes it extra impressive to me) https://twitter.com/b0rk/status/954366146505052160/photo/1
- 🔎Julia Evans🔍 (@b0rk)OTOH, the manual suffers the same problem, and fixing that is hard. Other times, the real problem lies in the excess complexity of the underlying features.
(For instance, the manual doesn't document well how cbn
and simpl
differ, but arguably many of those differences are bugs.)
I think even just applying tips from https://www.cs.utexas.edu/~wcook/presentations/Writing.pdf would help a lot; the original book (https://www.amazon.com/Style-Clarity-Chicago-Editing-Publishing/dp/0226899152) helped me learn to write much more clearly, early in my PhD
Paolo Giarrusso said:
Coq is telling you that mylength is not recursive. That’s because it calls length, while maybe you wanted to call mylength?
Ah, silly mistake on my part, thanks.
I think a system for good error messages should be at least partially formalized, e.g., there should be some kind of "refutation calculus" or "incorrectness logic" that the system could use to mechanically separate and minimize problems
Last updated: Oct 13 2024 at 01:02 UTC