How do I get identifiers in Coq to link correctly?

[JasonGross]

I'd like to be able to click on an identifier in code to jump to it's definition, and click on modules that are Required to jump to their definition. (For example, in https://hott.github.io/HoTT/alectryon-html/HoTT.Classes.interfaces.naturals.html) Additionally, I'd like for the coqdoc generated index links to work (https://hott.github.io/HoTT/alectryon-html/) or else for Alectryon to generate an index for me with links that work. How do I make this happen?

[cpitclaudel]

I'd love that as well. For that to work, you need to feed the relevant info to Alectryon in some way: either using glob files, or by getting SerAPI to produce it.

The issue on the SerAPI side is here: ejgallego/coq-lsp#330

The SerAPI option would be better, because it would be sound (the thing that Coqdoc currently does is not perfect: it sometimes gets hyperlink within a file wrong. But if it takes too much work (@ejgallego was mentioning this in the previous issue), then going with glob files might work.

[ejgallego]

I'm working on a h̶a̶c̶k̶ fix for ejgallego/coq-lsp#330 , at least to the point that it will be useful for Alectryon ; I think that is a good moment to fix that.

As I mentioned I'd like to provide a kind of more principled API for these kind of queries, but for now I will make available all the information that coqdoc receives via .glob files; that is still severely lacking but it is easy to grab (in a hacky way).

In fact, if you look at SerAPI's source you can see the plan to expose this info was there since the beginning, I just didn't finish it because as you will soon see the presentation of id resolution information is far from satisfactory :/

[ejgallego]

[The more principled way is actually a true database of Coq documents, but that will be available not too soon]

[jhaag]

Are there any updates on a principled - or hacky - solution to incorporating a coqdoc index (and coqdoc-style cross-linking of identifiers) into an alectryon project?