Stream: Coq devs & plugin devs

Topic: Location of errors (regression/change 8.15


view this post on Zulip Enrico Tassi (Jul 20 2022 at 15:10):

In Elpi I do raise a CError.user_err ~loc "..." and that loc may mention a file name which is not the name of the command.
I mean, in file a.v, line 5, I do call a coq-elpi command which parses file b.elpi, and the parse error is turned into a `CErrors.user_error ~loc:{... b.elpi...}.

The best I could get is

File "./theories/derive/eqb.v", line 54, characters 0-25:
Error:
File "/home/gares/LPCIC/fast-eqb/apps/derive/elpi/eqb.elpi", line 152, column 17, character 6418:
Term expected, got keyword.

It would be nice if Coq did not think my location is "less fine" than his I guess the culprit is Loc.finer (which considers command location finer than exception location if both are present and the file names don't match).

view this post on Zulip Gaƫtan Gilbert (Jul 20 2022 at 15:19):

this is the correct behaviour though, the failing command is in file a.v not b.elpi

view this post on Zulip Enrico Tassi (Jul 20 2022 at 15:35):

Well, then CErrors ~loc has a weird semantics, since the loc you pass is not necessarily the one it is displayed

view this post on Zulip Enrico Tassi (Jul 20 2022 at 15:36):

(and loc is optional...)

view this post on Zulip Enrico Tassi (Jul 20 2022 at 15:37):

IMO the intent was to check that both locs had a file name, or neither had it

view this post on Zulip Enrico Tassi (Jul 20 2022 at 15:37):

not that, if they had it, it was the same.

view this post on Zulip Enrico Tassi (Jul 20 2022 at 15:41):

Here a non Elpi specific example:

gares@ollypat:~/LPCIC/fast-eqb$ echo "Load \"b.v\"." > a.v
gares@ollypat:~/LPCIC/fast-eqb$ echo "Goal False. apply I." > b.v
gares@ollypat:~/LPCIC/fast-eqb$ coqc -R . xx a.v
File "./a.v", line 1, characters 0-11:
Error: Unable to unify "True" with "False".

Last updated: Feb 06 2023 at 19:03 UTC