jump to definition

[gares]

we need a libobject which populates a map kername -> loc (where loc contains a file name relative to the logical path)

mathcomp.ssreflect.ssrnat.len -> mathcomp.ssreflect + ssrnat.v + loc Coq.Init.Peano.le -> Coq.Init + Peano.v + loc

The one asks Coq where the logpath is mapped from, eg mathcomp.ssreflect -> $coqlib/user-contribs/mathcomp/ssreflect/, and the can generate the link file:///$coqlib/user-contribs/mathcomp/ssreflect/ssrnat.v

The libobject should be a bit down, since we also need to get links to generated stuff, eg foo_rect (and point to Inductive foo).

In response to the request https://microsoft.github.io/language-server-protocol/specification#textDocument_declaration one (re)globalized the AST we have in the document module, gets the kernel name, looks it up in the map, and generates the link. It is not always possible to "globalize" a vernac, since sometimes (eg Inductive/Record) it is messed up with interpretation. Possibilities:

• do it easy when possible, support only some sentences, eg Definition and Theorem and tactic
• have ad-hoc globalization code for inductive (take it from Coq-Elpi) and see if it can be pushed back upstream or not
• do the coqdoc hack: re-run the sentence logging 'loc -> kername' (dumpglob supports streaming to a non-file, IIRC). This has the nice effect of workings in all cases, but can be more expensive, and suffers from the ltac repeat t returning a gazillion of hits

[SkySkimmer]

Is there a way to get the current loc from declare-ish?

Then one asks Coq where the logpath is mapped from

That's not necessarily unique, we should ask where the file is mapped from instead (you can have -Q foo1 foo -Q foo2 foo and then foo.bar may be foo1/bar.v or foo2/bar.v)

For functors

Module F(A:T). 
Definition bla := ...
End F.
Module M := F X.

looking up M.bla should point to line 2 (Defininition ...) IMO To do this we keep DirPath.t * Loc.t

If we want to have an additional pointer to the Module := line we would need to do something at functor application too, not sure how easy that is.

[gares]

I did some "experiments" with this idea in Coq-Elpi (using a few hacks on top of 8.13). Since https://github.com/coq/coq/pull/13844 is merged commands get their loc in input, and could store a libobject which for example links one or more GlobRef.t to that loc.

This is what I could get in the context of the HB.about https://github.com/math-comp/hierarchy-builder/pull/227 command:

IMO, at least for the easy case of Definition/Lemma and Inductive, we can try to add this libobject. WDYT @SkySkimmer ?

[SkySkimmer]

IMO, at least for the easy case of Definition/Lemma and Inductive, we can try to add this libobject. WDYT @SkySkimmer ?

It makes sense to me.

I guess you used Loc.t so there are the same limitations with relocated / installed files as Jim had for the ltac debugger.

Proof of concept: https://github.com/coq/coq/commit/3f02b363b29ee2852461430e9a5ae46bb96b9ae6 (note that the test suite output/ rewrites all filenames to "stdin" for some reason)

[RalfJung]

This would help a lot to get vscoq on par with what is typically expected in a modern IDE. :)

AFAIK there are ways to get jump-to-definition in emacs with Company Coq, or did I imagine that? Could vscoq use the same approach for this?

[gares]

Iirc there is a way to open the file, and maybe there is code already for that. Going to the correct line requires some work, even if the outline (on the left panel) can jump to any definition within the same file.