refman: generate JSON indices

[shilangyu]

• Added / updated documentation.

Goal: improving editor tooling for Rocq.

Motivation

While some things can be collected by semantic analysis (such as user defined or library defined lemmas/definitions), a large part of core Rocq are compiler builtins. This includes commands (like Hint Rewrite), options (like Set Printing All), Ltac1 tactics (like eapply), and even attributes (like #[refine]).

While the grammar for these things could be extracted from Print Grammar, the documentation is left completely disjoint. I believe having documentation in the editor is important. To achieve this goal, I first extend the doc generator for the official Rocq documentation to additionally generate JSON metadata description of all builtins. Then, I use those metadata files (called "indices") to serve completions to the user in a best-effort manner.

See related discussion and these generated JSON files in VsRocq: rocq-prover/vsrocq#1251

Implementation

I modify the Sphinx Rocq domain python generator to not only output the final HTML/PDF files of the entire documentation, but to additionally output those JSON indices. By directly inspecting the source documentation RST files, I can extract the grammar and documentation of builtins. The can be generated with make refman-indices.

Known limitations

The collected documentation for builtins can have wonky formatting. For example, sometimes the documentation can have plain-text ascii tables which do not render well. This can be improved with further heuristics.

Discussion

It was suggested to me to open the PR with this generator here and to discuss possible ways for this (or something similar) to be integrated into the documentation pipeline. The current implementation feels hacky to me, yet it undeniably is enough to already serve pretty good completions in an editor (see VsRocq PR's demo video).

I am very open to hearing alternative implementation strategies.

cc: @SkySkimmer @gares

[SkySkimmer]

I believe having documentation in the editor is important.

I'm not sure I agree, especially when what the editor gets is this auto mangled output.

[gares]

I think it is very useful to have a link to the full doc, and also to have an excerpt of the doc.
I do have (the latter) for other PL in vscode, and it is quite nice (e.g. when the name is not that clear).

I don't know if the refman clearly separates a short intro to commands/tactics to the full doc (with examples, etc).

About the bad rendering, maybe it is just simpler to remove the parts that are not "plain text".

[gares]

Ci is now passing:

Could not import extension rocqrst.rocqdomain (exception: cannot import name 'Self' from 'typing' (/usr/lib/python3.10/typing.py))

[SkySkimmer]

Maybe worth bringing this up in a rocq call to get more opinions.

---

CI failure is probably some python version issue

[shilangyu]

Maybe worth bringing this up in a rocq call to get more opinions.

That would be great. I am open to any path that would allow for easier editor integration.

CI failure is probably some python version issue

Yes it is. Is there a strict python version requirement? Otherwise I can easily just replace the new APIs with older ones.

[SkySkimmer]

The "base" docker image currently uses ubuntu LTS 22.04 and gets whatever python comes with it.
I think we could update it to a newer LTS if it's convenient (IIUC 24.04 is LTS, 26.04 is too recent to use for our minimal versions).
Using older python APIs is also fine.

[SkySkimmer]

to add a rocq call topic see infos in https://github.com/coq/coq/wiki/Rocq-Calls

[SkySkimmer]

Suggested change

	$(WITHPYPATH) dune exec -- sphinx-build -q -W -b indices doc/sphinx doc/refman-indices
	$(WITHPYPATH) $(WITHJOBS) dune exec -- sphinx-build -q -W -b indices doc/sphinx doc/refman-indices