feat: jump to definition proof of concept

[rtetley]

WIP

cf coq/coq#19584

[gares]

Changes to coq look good too.
I wonder if there is a way to circumvent jumping to dune's copy of the sources.
I mean, should the logic be in Coq or here?
@SkySkimmer added the print of the Loc to a user visible message, so I guess it should be in Coq

[SkySkimmer]

@SkySkimmer added the print of the Loc to a user visible message, so I guess it should be in Coq

That logic is on the loc -> pp side though, vscoq only calls the qualid -> loc part from coq and does the rest on its own.

[SkySkimmer]

Suggested change

	match parse_entry st loc (Pcoq.Prim.smart_global) pattern with
	match parse_entry st loc Pcoq.Prim.qualid pattern with

since you're only using the AN case of smart_global

[gares]

It may still make sense to have the api on the coq side and let vscoq call it on the loc, no?

Anyway, good job!

[YaZko]

I wonder if there is a way to circumvent jumping to dune's copy of the sources.

I do not know if it's feasible, but as a user that would be fantastic if possible. Company-coq does indeed jumps to dune source, and it has always been a major pain.

[TheoWinterhalter]

I guess in the meantime something that works in most cases but not all is better than nothing?

[SkySkimmer]

this will need updating as I moved get_loc and made it apply to more than constants
something like

Suggested change

	begin match Nametab.locate qid with
	| ConstRef x -> begin match Declare.get_loc x with
	let extref = Nametab.locate_extended qid in
	match Nametab.cci_src_loc extref with

should work

[SkySkimmer]

Not sure how well this works with an editable document, I mean start with

(* some comment *)
Definition foo := 0.

Check foo.

evaluate the Definition, then edit the comment, then jump to def of the foo in Check

if editing the comment doesn't force re-evaluating the Definition then the loc will be wrong, but we don't want to re execute after editing comments (or whatever other edits we can detect as being trivial)

[gares]

That is certainly true, although it seems a minor problem in practice.

I'm thinking loud here: if we manage to perform some pieces of the globalization phase at parse time, then parsing "Definition foo := ..." could tell us that we will generate Some.Logical.Path.foo and we could store the KN->loc map in a synterp summary (rather than an interp one). We could complement the map at interp time with interp-time-generated stuff we really want to be precise, and that part would need to be shifted/shiftable by the UI when it tries to reuse an old state on a new text. Exactly as we do for diagnostics.

In a way, since the map is about locs, it should be part of the parsing state, not the interp one.

[SkySkimmer]

I'm thinking loud here: if we manage to perform some pieces of the globalization phase at parse time

That's impossible IMO

In a way, since the map is about locs, it should be part of the parsing state, not the interp one.

The map is about objects like globrefs which are part of the interp state.

[gares]

That's impossible IMO

AFAIK synterp already computes the current modpath. From that one can compute the final KN of "foo". Am I missing something? (I know today the kn data type is generated using the env, etc... but in principle we know all the data to compute it even without the env)