Hi,

coq-doc fails to build in up-to-date bookworm and sid environments.

bookworm:

Running[3871]: (cd _build/default/doc && /usr/bin/env sphinx-build -q -q -b latex sphinx refman-pdf)
Command [3871] exited with code 2:
$ (cd _build/default/doc && /usr/bin/env sphinx-build -q -q -b latex sphinx refman-pdf)

Exception occurred:
  File "/usr/lib/python3/dist-packages/sphinx/writers/latex.py", line 759, in visit_desc_content
    assert self.in_desc_signature
AssertionError
The full traceback has been saved in /tmp/buildc9edcc.dune/sphinx-err-9j2y314n.log, if you want to report the issue to the developers.
Please also report this if it was a user error, so that a better error message can be provided next time.
A bug report can be filed in the tracker at <https://github.com/sphinx-doc/sphinx/issues>. Thanks!
ANTLR runtime and generated code versions disagree: 4.9.1!=4.7.2
Duplicate cmd name:  Extraction
Duplicate exn name:  Not equal
Duplicate exn name:  Not equal (due to universes)
Duplicate tacn name:  first (ssreflect)
Duplicate tacn name:  have
Duplicate tacn name:  move (ssreflect)
Duplicate tacn name:  apply (ssreflect)
Duplicate tacn name:  under
Duplicate tacn name:  over
Duplicate tacn name:  wlog
Duplicate tacn name:  set (ssreflect)
Duplicate tacn name:  unlock
Duplicate tacn name:  congr
Duplicate cmd name:  Hint View for apply
Duplicate cmd name:  Prenex Implicits
Duplicate exn name:  Not the right number of missing arguments
Duplicate exn name:  No such hypothesis in current goal
Duplicate exn name:  No such hypothesis
Duplicate exn name:  ‘ident’ is used in the hypothesis ‘ident’
Duplicate exn name:  No such hypothesis
Duplicate exn name:  No such hypothesis
Duplicate exn name:  ‘ident’ is already used
Duplicate exn name:  No such assumption
Duplicate exn name:  No focused proof (No proof-editing in progress)
Duplicate exn name:  Not an inductive product
Duplicate exn name:  No primitive equality found

sid:

Command [1243] exited with code 1:
$ (cd _build/default && tools/configure/configure.exe -no-ask -native-compiler no -bin-annot)
ocamlfind: Package `zarith' not found
Error while running '/usr/bin/ocamlfind query zarith -format %v' (exit code 2)
Configuration script failed!
File "interp/dune", line 6, characters 12-18:
6 |  (libraries zarith pretyping))
                ^^^^^^
Error: Library "zarith" not found.
Hint: try:
  dune external-lib-deps --missing --display verbose @refman-html @refman-pdf
make[1]: *** [debian/rules:9: override_dh_auto_build] Error 1
make[1]: Leaving directory '/build/coq-doc-8.15.0'
make: *** [debian/rules:4: binary] Error 2

Hi Julien!

Actually the issue is in coq-doc because it's monkey-patching one of Sphinx
methods, and the code is based on old version of Sphinx.

I submitted a pull request upstream to rebase the monkey-patched version on
top of the new version of that method (see Forwarded link). With that patch
coq-doc builds successfully.

So reassigning back to coq-doc.

Hi,

this bug is fixed in unstable and testing, so it shouldn't stay around
any longer.

Cheers,

J.Puydt