cpitclaudel
commented
2 months ago Duplicate of https://github.com/cpitclaudel/alectryon/issues/27 I think?
It would be really nice, indeed. What's needed for this is either:
- Extending Alectryon to parse glob files, which is a pain and doesn't work within one reST or Markdown file (it only works for .v files).
- Extending the protocol to return that information (happened to some degree in coq-lsp, but Alectryon doesn't speak LSP right now)
Then it's a matter of formatting that info in the right ways.
This is probably doable but none of the examples in the gallery illustrate how to do it, which suggests that it's not obvious how to do it.
A quick scan through this page https://coq.inria.fr/doc/V8.19.2/stdlib/Coq.Init.Datatypes.html#bool shows that there are many, many hyperlinks in the page, it is very easy to go to the definition of something when you see it in a proof and you don't know what it means. I think this is really an important property of literate programming, to easily go to the definition of something you are reading.
Currently
:coqid:and its extensions are only usable outside the Coq code, so if you want to have your page link to definitions it has to be outside of the Coq code itself. This seems like it would make the text more verbose. So is it possible to make Coq identifers be clickable as links to go to their definition?