Stream: Coq devs & plugin devs

Topic: Building Sphinx documentation


view this post on Zulip Janno (May 15 2020 at 10:33):

@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.

view this post on Zulip Kenji Maillard (May 15 2020 at 10:43):

I think you need to pass some options as explained in doc/README.md:

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

view this post on Zulip Janno (May 15 2020 at 10:50):

Thanks! (How embarrassing.. Maybe one day I'll learn to read documentation all the way to the end.)

view this post on Zulip Théo Zimmermann (May 15 2020 at 12:32):

Well, the fact that you have warnings still mean that you are hitting a bug.

view this post on Zulip Théo Zimmermann (May 15 2020 at 12:33):

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.

view this post on Zulip Théo Zimmermann (May 15 2020 at 12:34):

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).

view this post on Zulip Théo Zimmermann (May 15 2020 at 12:37):

Here it is: https://gitter.im/coq/coq?at=5eb3e4329f0c955d7dace2ba

view this post on Zulip Théo Zimmermann (May 15 2020 at 12:37):

Could you please open an issue with the Sphinx version you installed?

view this post on Zulip Janno (May 15 2020 at 12:38):

Sure!

view this post on Zulip Théo Zimmermann (May 15 2020 at 12:38):

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.

view this post on Zulip Janno (May 15 2020 at 12:53):

Here's the issue: https://github.com/coq/coq/issues/12332.


Last updated: Oct 16 2021 at 03:02 UTC