Accessing fully qualified names when printing (for hyperlinking support in Alectryon)

[cpitclaudel]

Hi Emilio.

This is a follow up to https://github.com/coq/coq/issues/4834#issuecomment-655766329 (thanks for the quick response!)

One thing Alectryon is missing compared to coqdoc is hyperlinking abilities. I'd like to (1) be able to link to definitions that appear in Alectryon blocks and (2) be able to link to documentation generated by coqdoc. To support this, I think I need to support two scenarios:

1. I have a bit of input code: Definition x := 1.; I need to realize that this defines the symbol MyFile.x (in turn this probably means that I need to pass SerAPI a -topname?

2. I have a bit of input code (Goal 1 + 1 = 2.) or a bit of output (1 + 1 = 2, part of a SerAPI Goal); I need to realize that "+" is Coq.Init.Nat.add.

I can almost get this information with SerAPI If I ask for CoqSer output (it gives me fully qualified names, which is great). But CoqSer results don't include info on notations, so I can't produce pretty-printed hyperlinked output with that.

There's also CoqPp output, and there the Pp_tags that say things like "notation". But there are no tags for FQNs.

Maybe we could have a separate mode that returns CoqPp structures with meta information in new Pp_Tags? (But then I'd have to reimplement the box layout algorithm on my side). Or maybe we could return meta info for spans of formatted output (but that might tricky to implement?). Or maybe there's something completely different that I didn't think of?

Going the annotated Pp_tag route means that we can also include stuff like syntax-highliting information with the same mechanism at a future point, which would be pretty sweet.

Looping in @Ptival who has stuff like this working on top of jsCoq in his cool online demo in the past.

Hope you're doing well! Clément.

[Ptival]

Hi Clément.

Sadly, I believe I had pretty much taken the unpleasant approach of re-implementing the pretty-printing myself for dealing with notations, and I don't remember having a good story on fully-qualified names. But what you describe seems like it'd be useful indeed. I assume Emilio will have some better idea of what the nicest way of conveying all this information is.

[ejgallego]

There is a plan to handle those properly, and some people have been already waiting for an embarrassing amount of time for me to finish the work :/ I hope I can get some cycles to work on this next week.

[cpitclaudel]

Thanks Emilio! Looking forward to it. Ping me if you need help beta-testing :)

[ejgallego]

Hi @cpitclaudel ,

I can almost get this information with SerAPI If I ask for CoqSer output (it gives me fully qualified names, which is great). But CoqSer results don't include info on notations, so I can't produce pretty-printed hyperlinked output with that.

I'm looking into this, what do you mean here exactly, how do you get those qualified names?

I have a bit of input code (Goal 1 + 1 = 2.) or a bit of output (1 + 1 = 2, part of a SerAPI Goal); I need to realize that "+" is Coq.Init.Nat.add.

Umm, this should be possible, we do something similar in jsCoq using Pp.t plus a bit of extended protocol, but indeed if you want to look at the AST you will get a CNotation node that you can resolve with Query, not the location likely tho.

Definitively I'd like to extend Pp.t so it does actually provide all the meta info that would be necessary, but that will require changes in Coq.

Let's assume that for point 2, you either hack something with current annotations [as done in jsCoq], or you grab CNotation nodes.

Let's go back to 1 then, unfortunately there is no good support for Coq to do this yet, but we can grab the glob information that is used by coqdoc and attach it to each sentence, this should provide you with quite a bit of info.

So let's implement this and see what we get.

[cpitclaudel]

I'm looking into this, what do you mean here exactly, how do you get those qualified names?

Sorry, you're right, I don't actually get FQNs. I misread some output.

Let's go back to 1 then, unfortunately there is no good support for Coq to do this yet, but we can grab the glob information that is used by coqdoc and attach it to each sentence, this should provide you with quite a bit of info.

Sounds great. Also now that I think of it, I wonder if the best approach wouldn't be the following:

• For constants, link to their definition. The current PpSer format includes FQNs already, so we need to connect that to the glob data.
• For notations, link to the definition of the notation. I don't need to resolve + to Init.Nat.add; I just need to know that the notation _ + _ was defined in file theories/Init/Peano.v:92.

So the current output looks like this:

Module Abc.
  Definition xyz := 1.
End Abc.
Goal Abc.xyz + Abc.xyz = 1.

'("CoqExpr"
  (("v"
    ("CNotation"
     ("InConstrEntrySomeLevel" "_ = _")
     (((("v"
         ("CNotation"
          ("InConstrEntrySomeLevel" "_ + _")
          (((("v"
              ("CRef"
               (("v" 
                 ("Ser_Qualid"
                  ("DirPath"
                   (("Id" "Abc")))
                  ("Id" "xyz")))
                ("loc" nil))
               nil))
             ("loc" nil))
            (("v"
              ("CRef"
               (("v"
                 ("Ser_Qualid"
                  ("DirPath"
                   (("Id" "Abc")))
                  ("Id" "xyz")))
                ("loc" nil))
               nil))
             ("loc" nil)))
           nil nil nil)))
        ("loc" nil))
       (("v"
         ("CPrim"
          ("Numeral" "SPlus"
           (("int" "1")
            ("frac" "")
            ("exp" "")))))
        ("loc" nil)))
      nil nil nil)))
   ("loc" nil)))

We have Ser_Qualids already, which is great; we'd need these and the CNotations to include location info.

So let's implement this and see what we get.

:tada:

Oh, btw, we can add Alectryon to the list of SerAPI clients now :)

[ejgallego]

Oh, I see, actually the output here has qualids, because this is an AST synthethized from kernel terms; this also means that unfortunately locations are missing; I wonder how to add locations to a "reversed" term.

You still have to resolve to qualids if looking at the regular, from-parser AST, but I think glob files will do exactly that?

[ejgallego]

72 should help with this.

[ejgallego]

Finally Flèche can resolve symbols across a workspace. As of now this is used in:

• jump to definition
• hover (will show full name and file where it is defined)

Happy to expose this in more structured ways.

[cpitclaudel]

Thanks! Is there a way to access that info from the LSP server?

[ejgallego]

Thanks! Is there a way to access that info from the LSP server?

• textDocument/definition will provide you with the location of the symbol at point, but that not fit well for your use case
• textDocument/hover will print the full name and location, and also the documentation soon (PR almost done), however that is Markdown which is not very convenient.

So I am not sure there is something in the standard that would fit Alectryon's use case exactly, maybe we could hack workspace/symbol or textDocument/documentSymbol ?

Not sure if LSP provides exactly what you would need.

Adding a request coq/symbolInformation(symbol) that would return a record with the info (documentation, file, position, full name, and maybe some more properties) would be pretty easy (just writing the boilerplate), so maybe we could spec that, how does for example the Lean backend get this info? If we spec that properly, there should be no problem in sharing this across Coq and Lean (as we do with progress info for example).

Tho for Alectryon a small fcc plugin could make more sense, so Alectryon calls fcc --plugin=alectryon-info and a .json file for the document with all the info is built.

WDYT? I'd be happy to adapt to match in the best way possible Alectryon requirements.

[cpitclaudel]

So I am not sure there is something in the standard that would fit Alectryon's use case exactly,

I'm almost certain that there isn't, indeed. Same issue as for breaking up the document into sentences.

Adding a request coq/symbolInformation(symbol) that would return a record with the info (documentation, file, position, full name, and maybe some more properties)

Tricky, because I don't have the required symbol to start with (that is, I don't have symbol boundaries or a "point" to query information for, I just have the whole document.

Tho for Alectryon a small fcc plugin could make more sense

What is FCC? But yes, that potentially sounds good.

how does for example the Lean backend get this info?

The Lean backend uses LeanInk, but AFAIK it doesn't link to identifiers.

(as we do with progress info for example).

Ah, is there something shared between Coq and Lean for progress info? Neat.

[ejgallego]

So I am not sure there is something in the standard that would fit Alectryon's use case exactly,

I'm almost certain that there isn't, indeed. Same issue as for breaking up the document into sentences.

For that you can use coq/getDocument , see protocol docs; IMHO should work OK.

Tricky, because I don't have the required symbol to start with (that is, I don't have symbol boundaries or a "point" to query information for, I just have the whole document.

Oh, I was under the impression you had already the symbol at hand, as you were printing goals.

How were you getting the info before? Both coq/goals and coq/getDocument can provide an Ast if that's what you want, or even better, we can implement an Ast.t -> Id.t With_range.t list filter that would extract from the Ast the identifiers you need. But note that sadly this won't work for goals in Coq as they don't properly have an Ast (we could improve Coq's unparsing, but that'd be quite a lot of work)

What is FCC? But yes, that potentially sounds good.

I need to improve the info (I'm on it). coq-lsp checking engine is independent from LSP; the engine, named Flèche, does support other modes. fcc is compiler that calls Fleche to compile a Coq document without spawning a full lsp client. You can write plugins to it, for example to do stuff when a document completes checking, see for example goaldump

The Lean backend uses LeanInk, but AFAIK it doesn't link to identifiers.

Thanks for the pointer, I'll have a look!

Ah, is there something shared between Coq and Lean for progress info? Neat.

Not really shared, but I am trying to stay as close to the standard as possible, and after that, to extensions used in other systems, so I re-used their protocol implementation for that as I didn't see reason to deviate (see upstream LSP issue about ITPs)

[ejgallego]

I need to run now, but I think it should be possible to write CoqInk using the Flèche API; recently a few people have shown interested in using Flèche's API in a similar way to Lean's API, and actually while Flèche needs to get a couple of adjustments, it should be possible to port Lean-based tools to Flèche quite fast.

[cpitclaudel]

For that you can use coq/getDocument , see protocol docs; IMHO should work OK.

Thanks a lot, I will look!

How were you getting the info before?

I don't currently have hyperlinks :) Looking forward to adding them!

[cpitclaudel]

I think it should be possible to write CoqInk using the Flèche API

I haven't looked at the API of LeanInk in depth, but that could be nice.