Enrico Tassi (Jul 20 2022 at 15:10): 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).
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
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
Enrico Tassi (Jul 20 2022 at 15:36):(and loc is optional...)
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
Enrico Tassi (Jul 20 2022 at 15:37):not that, if they had it, it was the same.
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: Jun 09 2023 at 08:01 UTC