When a .v file accumulates an external .elpi file (via Extra Dependency
Elpi Accumulate File) and that .elpi file contains a Coq term
quotation (e.g. {{ nat }}) that gets elaborated, the R (reference) entry
written to the .v file's .glob uses the byte offset of the identifier
inside the .elpi file, not inside the .v file. The two files have
unrelated contents/lengths, so the recorded span is either garbage or, as in
the example below, entirely out of range for the .v file.
This breaks any tool that relies on .glob offsets being valid spans of the
.v file the entry is attributed to (coqdoc-style HTML generation,
"jump to definition" in editors, etc.).
Environment
- Rocq: 9.1.1
- rocq-elpi:
upstream/master @ 5ad969a4
Minimal reproduction
mylib.elpi
main _ :- T = {{ nat }}, coq.say T.
test.v
From elpi Require Import elpi.
From Repro Extra Dependency "mylib.elpi" as mylib.
Elpi Command mytest.
Elpi Accumulate File mylib.
Elpi mytest.
$ rocq compile -R . Repro -dump-glob test.glob test.v
$ cat test.glob
DIGEST NO
FRepro.test
R25:28 elpi.elpi <> <> lib
R17:19 Corelib.Init.Datatypes <> nat ind
R17:19 claims that bytes 17–19 of test.v reference nat. But it is a part of "Import" (" I").
The offset is really the position of nat inside mylib.elpi, not test.v.
Related links
When a
.vfile accumulates an external.elpifile (viaExtra DependencyElpi Accumulate File) and that.elpifile contains a Coq termquotation (e.g.
{{ nat }}) that gets elaborated, theR(reference) entrywritten to the
.vfile's.globuses the byte offset of the identifierinside the
.elpifile, not inside the.vfile. The two files haveunrelated contents/lengths, so the recorded span is either garbage or, as in
the example below, entirely out of range for the
.vfile.This breaks any tool that relies on
.globoffsets being valid spans of the.vfile the entry is attributed to (coqdoc-style HTML generation,"jump to definition" in editors, etc.).
Environment
upstream/master@5ad969a4Minimal reproduction
mylib.elpitest.vR17:19claims that bytes 17–19 oftest.vreferencenat. But it is a part of "Import" (" I").The offset is really the position of
natinsidemylib.elpi, nottest.v.Related links