Bug 2072116

Summary: coq fails to build latex docs with Sphinx 4.5.0
Product: [Fedora] Fedora Reporter: Karolina Surma <ksurma>
Component: coqAssignee: Alan Dunn <amdunn>
Status: CLOSED ERRATA QA Contact: Fedora Extras Quality Assurance <extras-qa>
Severity: unspecified Docs Contact:
Priority: unspecified    
Version: rawhideCC: amdunn, loganjerry
Target Milestone: ---   
Target Release: ---   
Hardware: Unspecified   
OS: Unspecified   
Whiteboard:
Fixed In Version: coq-8.15.2-2.fc37 Doc Type: If docs needed, set a value
Doc Text:
Story Points: ---
Clone Of: Environment:
Last Closed: 2022-06-21 18:46:24 UTC Type: Bug
Regression: --- Mount Type: ---
Documentation: --- CRM:
Verified Versions: Category: ---
oVirt Team: --- RHEL 7.3 requirements from Atomic Host:
Cloudforms Team: --- Target Upstream Version:
Embargoed:
Bug Depends On:    
Bug Blocks: 2068924    
Attachments:
Description Flags
Full Sphinx traceback none

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

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.