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).
this is the correct behaviour though, the failing command is in file a.v not b.elpi
Well, then CErrors ~loc
has a weird semantics, since the loc you pass is not necessarily the one it is displayed
(and loc is optional...)
IMO the intent was to check that both locs had a file name, or neither had it
not that, if they had it, it was the same.
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: Jun 09 2023 at 08:01 UTC