Bug#1005920: closed by Debian FTP Masters <ftpmaster@ftp-master.debian.org> (reply to Julien Puydt <jpuydt@debian.org>) (Bug#1005920: fixed in coq-doc 8.15.0-3)
Le mercredi 23 février 2022 à 13:21 +0100, Andreas Beckmann a écrit :
> With all these B-D added, the build fails for me now with
>
> Running[3870]: (cd _build/default/doc && /usr/bin/env sphinx-build -q
> -W -b html sphinx refman-html)
> Command [3870] exited with code 2:
> $ (cd _build/default/doc && /usr/bin/env sphinx-build -q -W -b html
> sphinx refman-html)
>
> Warning, treated as error:
> /build/coq-doc-8.15.0/_build/default/doc/sphinx/index.rst:45:toctree
> contains reference to document 'zebibliography' that doesn't have a
> title: no link will be generated
> 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
>
> Not sure what exactly causes the failure ...
I tested the package on barriere.debian.org and a local schroot before
uploading, so I really don't get how that can fail. Those messages
aren't the real problem, as I got them a lot even when the build
succeeded.
And indeed it can be hard to tell what the exact problem is: you have
to take a look to CofRefMan.log and see what the complaints are about.
Sometimes it was just a question of too many warnings...
Guess what? Today, my local schroot fails, so I'll probably be able to
do something... again.
I admit that bug is stubborn: I already closed it twice and it's still
kicking.
But I'll get it in the end.
J.Puydt
Reply to: