@Théo Zimmermann I could use some help with coqdoc. (Writing here to avoid spamming the PR.)
Note that you have documentation on build dependencies here [..] Let me know if you need help beyond this.
I have installed all the required libraries but I think there must be a problem with my versions of the libraries maybe being too recent?
ANTLR runtime and generated code versions disagree: 4.8!=4.7.2 .. [Repeated a few thousand times] .. ANTLR runtime and generated code versions disagree: 4.8!=4.7.2 checking for /home/janno/src/coq/doc/sphinx/biblio.bib in bibtex cache... not found parsing bibtex file /home/janno/src/coq/doc/sphinx/biblio.bib... parsed 54 entries Warning, treated as error: /home/janno/src/coq/doc/sphinx/proof-engine/ltac2.rst:665:duplicate token description of coq:ltac2_term , other instance in proof-engine/ltac2
The first ANTLR warnings don't seem to be fatal on their own.
I think you need to pass some options as explained in
To build the Sphinx documentation without stopping at the first warning with the legacy Makefile, set `SPHINXWARNERROR` to 0 as such: SPHINXWARNERROR=0 make refman-html To do the same with the Dune build system, change the value of the `SPHINXWARNOPT` variable (default is `-W`). The following will build the Sphinx documentation without stopping at the first warning, and store all the warnings in the file `/tmp/warn.log`: SPHINXWARNOPT="-w/tmp/warn.log" dune build @refman-html
Thanks! (How embarrassing.. Maybe one day I'll learn to read documentation all the way to the end.)
Well, the fact that you have warnings still mean that you are hitting a bug.
The ANTLR one is annoying indeed, especially if repeated many times. Apparently you need an exact version. I have no idea if this is important or not and if we could simply disable the warning.
But the main problem is this duplicate token warning, which seems to be a bug of a particular version of Sphinx (it was already reported previously by someone else, let me see if I can find it).
Here it is: https://gitter.im/coq/coq?at=5eb3e4329f0c955d7dace2ba
Could you please open an issue with the Sphinx version you installed?
Switching to the one in the Dockerfile (1.8.0) or to another one that is known to work (2.2.2, 2.3.1) should fix this for you, in principle.
Here's the issue: https://github.com/coq/coq/issues/12332.
Last updated: Feb 02 2023 at 13:03 UTC