Bug 2072116 - coq fails to build latex docs with Sphinx 4.5.0
Summary: coq fails to build latex docs with Sphinx 4.5.0
Alias: None
Product: Fedora
Classification: Fedora
Component: coq
Version: rawhide
Hardware: Unspecified
OS: Unspecified
Target Milestone: ---
Assignee: Alan Dunn
QA Contact: Fedora Extras Quality Assurance
Depends On:
Blocks: 2068924
TreeView+ depends on / blocked
Reported: 2022-04-05 16:07 UTC by Karolina Surma
Modified: 2022-06-21 18:46 UTC (History)
2 users (show)

Fixed In Version: coq-8.15.2-2.fc37
Doc Type: If docs needed, set a value
Doc Text:
Clone Of:
Last Closed: 2022-06-21 18:46:24 UTC
Type: Bug

Attachments (Terms of Use)
Full Sphinx traceback (3.15 KB, text/plain)
2022-04-06 08:38 UTC, Karolina Surma
no flags Details

System ID Private Priority Status Summary Last Updated
Github sphinx-doc sphinx issues 10332 0 None open LaTeX docs build ends in failure with Sphinx 4.5.0 2022-04-07 14:01:54 UTC

Description Karolina Surma 2022-04-05 16:07:33 UTC
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):

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

Expected results:
The build is successful.

Comment 1 Karolina Surma 2022-04-06 08:38:17 UTC
Created attachment 1871008 [details]
Full Sphinx traceback

I've extracted the extended Sphinx traceback from the build data.

Comment 2 Karolina Surma 2022-04-07 14:01:55 UTC
I discussed this bug with Miro Hroncok and evaluated it as Sphinx regression. I opened the attached GH issue to Sphinx' upstream.

Comment 3 Karolina Surma 2022-04-21 11:22:00 UTC
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.

Comment 4 Jerry James 2022-04-21 20:00:13 UTC
Thank you for working with upstream and for keeping us informed.

Comment 5 Fedora Update System 2022-06-21 18:44:16 UTC
FEDORA-2022-5fc4d80950 has been submitted as an update to Fedora 37. https://bodhi.fedoraproject.org/updates/FEDORA-2022-5fc4d80950

Comment 6 Fedora Update System 2022-06-21 18:46:24 UTC
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.

Note You need to log in before you can comment on or make changes to this bug.