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

[cpitclaudel]

trafficstars

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?