Stream: Coq devs & plugin devs

Topic: Intros' error message


view this post on Zulip Hugo Herbelin (Jul 31 2023 at 15:04):

In his talk on teaching Coq to undergraduate students at the Coq workshop, @Pierre Rousselin mentioned the crypticity of intros' error message, that is, currently:

Goal True -> True.
intros H1 H2.
^^^^^^^^^^^^
Error: No product even after head-reduction.

or

Goal True.
intro.
^^^^^
Error: No product even after head-reduction.

or

Goal True.
intros H.
^^^^^^^^
Error: No product even after head-reduction.

or

Goal True.
intros (H1,H2).
^^^^^^^^^^^^^^
Error: No product even after head-reduction.

Pierre proposed "No more variables or hypotheses to introduce". We could actually have two variants, one with "more" and one without (as a matter of comparison, ssr's movesays "No assumption in True"). We should also probably highlight the introduction pattern that cannot be introduced when there is one. However, what would be the best way to attach a location to the error message. At some time, there was the idea that the tactics.mlfile should not mention locs. I guess the alternative is to carefully catch the error at places where it makes sense to attach a location. Any opinion?

view this post on Zulip Gaëtan Gilbert (Jul 31 2023 at 15:20):

At some time, there was the idea that the tactics.ml file should not mention locs.

Please explain more

I guess the alternative is to carefully catch the error at places where it makes sense to attach a location.

I think this may be already the case

view this post on Zulip Hugo Herbelin (Jul 31 2023 at 16:15):

Please explain more

PMP was reluctant at some time when I wanted to push the location of idents towards the place errors are raised.

I think this may be already the case

In the case of intros, the error is attached (only) to the tactic call.


Last updated: Jun 13 2024 at 04:03 UTC