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