Description of problem: coq doesn't build with Sphinx 4.5.0 (changelog: https://www.sphinx-doc.org/en/master/changes.html#id42). `make refman-pdf` tries to produce LaTex docs and fails. The error message leads back to Sphinx, which did make some changes to the file pointed out in the traceback (eg. https://github.com/sphinx-doc/sphinx/commit/6768577bd96053afd744ea1f229edbb287fd32d9 introduces 'in_desc_signature' attribute). It may or may not be a Sphinx regression, but I can't figure out on my own which one it is. Can you take it a look at this issue? Version-Release number of selected component (if applicable): 8.15.1-1 How reproducible: Always with Sphinx 4.5.0 (with Sphinx 4.4.0 the build is successful) Steps to Reproduce: $ mock -r fedora-rawhide-x86_64 --addrepo=https://download.copr.fedorainfracloud.org/results/ksurma/sphinx-4.5.0/fedora-rawhide-x86_64/ --no-clean your.src.rpm Actual results: make refman-pdf make[2]: Entering directory '/builddir/build/BUILD/coq-8.15.1' make --warn-undefined-variable --no-builtin-rules -f Makefile.build refman-pdf make[3]: Entering directory '/builddir/build/BUILD/coq-8.15.1' flock .dune.lock dune build --display=quiet --release @all-src cp -a _build_vo/default/doc/unreleased.rst doc # to fix when we move the sphinx build out-of-tree COQBIN="/builddir/build/BUILD/coq-8.15.1/_build/install/default/bin" COQLIB="/builddir/build/BUILD/coq-8.15.1/_build_vo/default//lib/coq/" sphinx-build -b latex \ -d doc/sphinx/_build/doctrees -W doc/sphinx doc/sphinx/_build/latex Running Sphinx v4.5.0 making output directory... done loading pickled environment... checking bibtex cache... up to date done Copying /builddir/build/BUILD/coq-8.15.1/doc/sphinx/index.latex.rst to /builddir/build/BUILD/coq-8.15.1/doc/sphinx/index.rst Copying /builddir/build/BUILD/coq-8.15.1/doc/sphinx/zebibliography.latex.rst to /builddir/build/BUILD/coq-8.15.1/doc/sphinx/zebibliography.rst building [mo]: targets for 0 po files that are out of date building [latex]: all documents updating environment: 0 added, 2 changed, 0 removed reading sources... [ 50%] index reading sources... [100%] zebibliography looking for now-outdated files... none found pickling environment... done checking consistency... done processing CoqRefMan.tex... index language/core/index language/core/basic language/core/sorts language/core/assumptions language/core/definitions language/core/conversion language/cic language/core/variants language/core/records language/core/inductive language/core/coinductive language/core/sections language/core/modules language/core/primitive addendum/universe-polymorphism addendum/sprop language/extensions/index language/extensions/evars language/extensions/implicit-arguments language/extensions/match user-extensions/syntax-extensions language/extensions/arguments-command addendum/implicit-coercions addendum/type-classes language/extensions/canonical addendum/program proof-engine/vernacular-commands proofs/writing-proofs/index proofs/writing-proofs/proof-mode proof-engine/tactics proofs/writing-proofs/equality proofs/writing-proofs/reasoning-inductives proof-engine/ssreflect-proof-language proofs/automatic-tactics/index proofs/automatic-tactics/logic addendum/micromega addendum/ring addendum/nsatz proofs/automatic-tactics/auto addendum/generalized-rewriting proofs/creating-tactics/index proof-engine/ltac proof-engine/ltac2 using/libraries/index language/coq-library addendum/extraction addendum/miscellaneous-extensions using/libraries/funind using/libraries/writing using/tools/index practical-tools/coq-commands practical-tools/utilities using/tools/coqdoc practical-tools/coqide addendum/parallel-proof-processing appendix/history-and-changes/index history changes zebibliography resolving references... done writing... failed Exception occurred: File "/usr/lib/python3.10/site-packages/sphinx/writers/latex.py", line 759, in visit_desc_content assert self.in_desc_signature AssertionError Expected results: The build is successful.
Created attachment 1871008 [details] Full Sphinx traceback I've extracted the extended Sphinx traceback from the build data.
I discussed this bug with Miro Hroncok and evaluated it as Sphinx regression. I opened the attached GH issue to Sphinx' upstream.
I've commented out the problematic assert and tried to rebuild coq with the same bad result. Truncated output: Latexmk: ====List of undefined refs and citations: Reference `language/core/sorts:term-algebraic-universe' on page 791 undefined on input line 80805 Reference `language/core/conversion:term-alpha-convertible' on page 791 undefined on input line 80806 Reference `language/core/basic:term-attribute' on page 791 undefined on input line 80807 Reference `proof-engine/ltac:term-backtracking' on page 791 undefined on input line 80810 Reference `proof-engine/ltac:term-backtracking-point' on page 791 undefined on input line 80811 Reference `proof-engine/tactics:term-backward-reasoning' on page 791 undefined on input line 80812 Reference `language/core/conversion:term-beta-redex' on page 791 undefined on input line 80813 And 1071 more --- see log file. Latexmk: If appropriate, the -f option can be used to get latexmk to try to force complete processing. Latexmk: Getting log file 'CoqRefMan.log' Latexmk: Summary of warnings from last run of *latex: Latex failed to resolve 1078 reference(s) =====Latex reported missing or unavailable character(s). =====See log file for details. Collected error summary (may duplicate other messages): pdflatex: Command for 'pdflatex' gave return code 1 Refer to 'CoqRefMan.log' for details CoqRefMan.log contains a lot of broken references and some returning error messages for the \pysigstopsignatures in question. Example fragment of log: LaTeX Warning: Hyper reference `language/core/basic:grammar-token-ident' on pag e 282 undefined on input line 1. ! Undefined control sequence. \pysigstopsignatures ...store@itemsep@and@parskip l.26217 \pysigstopsignatures The control sequence at the end of the top line of your error message was never \def'ed. If you have misspelled it (e.g., `\hobx'), type `I' and the correct spelling (e.g., `I\hbox'). Otherwise just continue, and I'll forget about whatever was undefined. This was reported to the issue open on Sphinx upstream.
Thank you for working with upstream and for keeping us informed.
FEDORA-2022-5fc4d80950 has been submitted as an update to Fedora 37. https://bodhi.fedoraproject.org/updates/FEDORA-2022-5fc4d80950
FEDORA-2022-5fc4d80950 has been pushed to the Fedora 37 stable repository. If problem still persists, please make note of it in this bug report.