Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

LaTeX documentation doesn't build with Sphinx 4.5.0 #15956

Closed
befeleme opened this issue Apr 27, 2022 · 3 comments · Fixed by #16193
Closed

LaTeX documentation doesn't build with Sphinx 4.5.0 #15956

befeleme opened this issue Apr 27, 2022 · 3 comments · Fixed by #16193
Labels
kind: documentation Additions or improvement to documentation. needs: triage The validity of this issue needs to be checked, or the issue itself updated. part: build The build system.
Projects
User documentation
Milestone
8.16.0

Comments

@befeleme
Copy link
Contributor

Description of the problem

When integrating Sphinx 4.5.0 to Fedora, we uncovered an issue with coq: the LaTeX documentation doesn't build correctly (as it did with previous Sphinx versions).
The investigation results were evaluated as likely regression in Sphinx and reported as sphinx-doc/sphinx#10332. The issue in question contains the insights from the RPM build.

Coq Version

coq 8.15.1
@Alizter Alizter added kind: documentation Additions or improvement to documentation. part: build The build system. needs: triage The validity of this issue needs to be checked, or the issue itself updated. labels May 6, 2022
@Alizter Alizter added this to Fixing in User documentation May 17, 2022
@xgqt
Copy link

xgqt commented May 31, 2022

CC @xgqt
Today, trying to bump Coq to version 8.15.2 in Gentoo I had the same issue.
https://dpaste.com/7CER4L2KR

@SnarkBoojum
Copy link
Contributor

Eh, trying to update coq-doc in Debian also brings this up.

I had no problem with the coq package since it doesn't contain the documentation for license reasons.

mitya57 added a commit to mitya57/coq that referenced this issue Jun 15, 2022
@mitya57
Fix coq#15956: error when building with Sphinx 4.5
d5568fc 
Unfortunately it breaks building with older versions.

The only way to fix this issue for all versions is to stop monkey-patching
and forward the fix to Sphinx upstream.
@mitya57 mitya57 mentioned this issue Jun 15, 2022
Merged
@mitya57
Copy link
Contributor

mitya57 commented Jun 15, 2022 •
edited

This happens because coq is monkey-patching visit_desc_signature method of sphinx.writers.latex.LaTeXTranslator. I opened a PR to fix this: #16193.

mitya57 added a commit to mitya57/coq that referenced this issue Jun 23, 2022
@mitya57
Fix coq#15956: error when building with Sphinx 4.5
c40ad6f
mitya57 added a commit to mitya57/coq that referenced this issue Jun 24, 2022
@mitya57
Fix coq#15956: error when building with Sphinx 4.5
cb04626
User documentation automation moved this from Fixing to Done Jul 5, 2022
@coqbot-app coqbot-app bot added this to the 8.16.0 milestone Jul 5, 2022
ppedrot pushed a commit to ppedrot/coq that referenced this issue Jul 21, 2022
@mitya57 @ppedrot
Fix coq#15956: error when building with Sphinx 4.5
a36b2a8 
(cherry picked from commit cb04626)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: documentation Additions or improvement to documentation. needs: triage The validity of this issue needs to be checked, or the issue itself updated. part: build The build system.
Projects
User documentation
Archived in project
User documentation
  
Done
Milestone
8.16.0
Development

Successfully merging a pull request may close this issue.

Fix error when building with Sphinx 4.5 mitya57/coq
5 participants
@mitya57 @SnarkBoojum @Alizter @befeleme @xgqt