Package: release.debian.org Severity: normal User: release.debian....@packages.debian.org Usertags: transition X-Debbugs-Cc: jpu...@debian.org X-Debbugs-Cc: Debian OCaml Maintainers <debian-ocaml-ma...@lists.debian.org>
Hi, I would like to upload coq 8.16.0+dfsg-1 to unstable ; that also means uploading a number of new versions for other packages: aac-tactics 8.16.0-1 coq-bignums 8.16.0-1 coq-dpdgraph 1.0+8.16-1 coq-elpi 1.15.5-1 coq-reduction-effects 0.1.4-2 coq-hammer 1.3.2+8.16-1 coq-unicoq 1.6-8.16-1 paramcoq 1.1.3+coq8.16-1 coq-hott 8.16-1 coq-equations 1.3-8.16-1 coq-gappa 1.5.2-4 coq-hierarchy-builder 1.3.0-2 coq-mtac2 1.4+8.16-1 coq-simple-io 1.7.0-3 coq-corn 8.16.0-1 coq-quickchick 1.6.4-2 mathcomp-analysis 0.5.3-2 and to just recompile a list of others : all 41 packages of the Coq ecosystem are involved! I would like to dput all new package versions and let the buildd trigger things in order. I checked all compilation would go well on my amd64 box. My experimental wanna-build script gave me something I'll paste below -- as you can guess it's a bit long. Just waiting for a "Go!", J.Puydt PS: nmu coq-deriving_0.1.0-1+b1 . ANY . -m 'Rebuild due to coq=8.16.0+dfsg-1 aac-tactics=8.16.0-1 coq-bignums=8.16.0-1 coq-dpdgraph=1.0+8.16-1 coq-elpi=1.15.5-1 coq-reduction-effects=0.1.4-2 coq-hammer=1.3.2+8.16-1 coq-unicoq=1.6-8.16-1 paramcoq=1.1.3+coq8.16-1 coq-hott=8.16-1 coq-equations=1.3-8.16-1 coq-gappa=1.5.2-4 coq-hierarchy-builder=1.3.0-2 coq-mtac2=1.4+8.16-1 coq-simple-io=1.7.0-3 coq-corn=8.16.0-1 coq-quickchick=1.6.4-2 mathcomp-analysis=0.5.3-2' dw coq-deriving_0.1.0-1+b1 . ANY . -m 'coq => 8.16.0+dfsg-1' nmu coqeal_1.1.1-1+b1 . ANY . -m 'Rebuild due to coq=8.16.0+dfsg-1 aac-tactics=8.16.0-1 coq-bignums=8.16.0-1 coq-dpdgraph=1.0+8.16-1 coq-elpi=1.15.5-1 coq-reduction-effects=0.1.4-2 coq-hammer=1.3.2+8.16-1 coq-unicoq=1.6-8.16-1 paramcoq=1.1.3+coq8.16-1 coq-hott=8.16-1 coq-equations=1.3-8.16-1 coq-gappa=1.5.2-4 coq-hierarchy-builder=1.3.0-2 coq-mtac2=1.4+8.16-1 coq-simple-io=1.7.0-3 coq-corn=8.16.0-1 coq-quickchick=1.6.4-2 mathcomp-analysis=0.5.3-2' dw coqeal_1.1.1-1+b1 . ANY . -m 'coq => 8.16.0+dfsg-1' dw coqeal_1.1.1-1+b1 . ANY . -m 'paramcoq => 1.1.3+coq8.16-1' dw coqeal_1.1.1-1+b1 . ANY . -m 'coq-bignums => 8.16.0-1' nmu coq-ext-lib_0.11.7-1 . ANY . -m 'Rebuild due to coq=8.16.0+dfsg-1 aac-tactics=8.16.0-1 coq-bignums=8.16.0-1 coq-dpdgraph=1.0+8.16-1 coq-elpi=1.15.5-1 coq-reduction-effects=0.1.4-2 coq-hammer=1.3.2+8.16-1 coq-unicoq=1.6-8.16-1 paramcoq=1.1.3+coq8.16-1 coq-hott=8.16-1 coq-equations=1.3-8.16-1 coq-gappa=1.5.2-4 coq-hierarchy-builder=1.3.0-2 coq-mtac2=1.4+8.16-1 coq-simple-io=1.7.0-3 coq-corn=8.16.0-1 coq-quickchick=1.6.4-2 mathcomp-analysis=0.5.3-2' dw coq-ext-lib_0.11.7-1 . ANY . -m 'coq => 8.16.0+dfsg-1' nmu coq-extructures_0.3.1-2 . ANY . -m 'Rebuild due to coq=8.16.0+dfsg-1 aac-tactics=8.16.0-1 coq-bignums=8.16.0-1 coq-dpdgraph=1.0+8.16-1 coq-elpi=1.15.5-1 coq-reduction-effects=0.1.4-2 coq-hammer=1.3.2+8.16-1 coq-unicoq=1.6-8.16-1 paramcoq=1.1.3+coq8.16-1 coq-hott=8.16-1 coq-equations=1.3-8.16-1 coq-gappa=1.5.2-4 coq-hierarchy-builder=1.3.0-2 coq-mtac2=1.4+8.16-1 coq-simple-io=1.7.0-3 coq-corn=8.16.0-1 coq-quickchick=1.6.4-2 mathcomp-analysis=0.5.3-2' dw coq-extructures_0.3.1-2 . ANY . -m 'coq => 8.16.0+dfsg-1' dw coq-extructures_0.3.1-2 . ANY . -m 'coq-deriving => 0.1.0-1+b2' nmu coq-interval_4.5.2-2 . ANY . -m 'Rebuild due to coq=8.16.0+dfsg-1 aac-tactics=8.16.0-1 coq-bignums=8.16.0-1 coq-dpdgraph=1.0+8.16-1 coq-elpi=1.15.5-1 coq-reduction-effects=0.1.4-2 coq-hammer=1.3.2+8.16-1 coq-unicoq=1.6-8.16-1 paramcoq=1.1.3+coq8.16-1 coq-hott=8.16-1 coq-equations=1.3-8.16-1 coq-gappa=1.5.2-4 coq-hierarchy-builder=1.3.0-2 coq-mtac2=1.4+8.16-1 coq-simple-io=1.7.0-3 coq-corn=8.16.0-1 coq-quickchick=1.6.4-2 mathcomp-analysis=0.5.3-2' dw coq-interval_4.5.2-2 . ANY . -m 'coq => 8.16.0+dfsg-1' dw coq-interval_4.5.2-2 . ANY . -m 'coq-bignums => 8.16.0-1' nmu coq-iris_4.0.0-1 . ANY . -m 'Rebuild due to coq=8.16.0+dfsg-1 aac-tactics=8.16.0-1 coq-bignums=8.16.0-1 coq-dpdgraph=1.0+8.16-1 coq-elpi=1.15.5-1 coq-reduction-effects=0.1.4-2 coq-hammer=1.3.2+8.16-1 coq-unicoq=1.6-8.16-1 paramcoq=1.1.3+coq8.16-1 coq-hott=8.16-1 coq-equations=1.3-8.16-1 coq-gappa=1.5.2-4 coq-hierarchy-builder=1.3.0-2 coq-mtac2=1.4+8.16-1 coq-simple-io=1.7.0-3 coq-corn=8.16.0-1 coq-quickchick=1.6.4-2 mathcomp-analysis=0.5.3-2' dw coq-iris_4.0.0-1 . ANY . -m 'coq => 8.16.0+dfsg-1' nmu coq-math-classes_8.15.0-3 . ANY . -m 'Rebuild due to coq=8.16.0+dfsg-1 aac-tactics=8.16.0-1 coq-bignums=8.16.0-1 coq-dpdgraph=1.0+8.16-1 coq-elpi=1.15.5-1 coq-reduction-effects=0.1.4-2 coq-hammer=1.3.2+8.16-1 coq-unicoq=1.6-8.16-1 paramcoq=1.1.3+coq8.16-1 coq-hott=8.16-1 coq-equations=1.3-8.16-1 coq-gappa=1.5.2-4 coq-hierarchy-builder=1.3.0-2 coq-mtac2=1.4+8.16-1 coq-simple-io=1.7.0-3 coq-corn=8.16.0-1 coq-quickchick=1.6.4-2 mathcomp-analysis=0.5.3-2' dw coq-math-classes_8.15.0-3 . ANY . -m 'coq => 8.16.0+dfsg-1' dw coq-math-classes_8.15.0-3 . ANY . -m 'coq-bignums => 8.16.0-1' nmu coq-menhirlib_20220210+ds-2 . ANY . -m 'Rebuild due to coq=8.16.0+dfsg-1 aac-tactics=8.16.0-1 coq-bignums=8.16.0-1 coq-dpdgraph=1.0+8.16-1 coq-elpi=1.15.5-1 coq-reduction-effects=0.1.4-2 coq-hammer=1.3.2+8.16-1 coq-unicoq=1.6-8.16-1 paramcoq=1.1.3+coq8.16-1 coq-hott=8.16-1 coq-equations=1.3-8.16-1 coq-gappa=1.5.2-4 coq-hierarchy-builder=1.3.0-2 coq-mtac2=1.4+8.16-1 coq-simple-io=1.7.0-3 coq-corn=8.16.0-1 coq-quickchick=1.6.4-2 mathcomp-analysis=0.5.3-2' dw coq-menhirlib_20220210+ds-2 . ANY . -m 'coq => 8.16.0+dfsg-1' nmu coqprime_8.15-1+b1 . ANY . -m 'Rebuild due to coq=8.16.0+dfsg-1 aac-tactics=8.16.0-1 coq-bignums=8.16.0-1 coq-dpdgraph=1.0+8.16-1 coq-elpi=1.15.5-1 coq-reduction-effects=0.1.4-2 coq-hammer=1.3.2+8.16-1 coq-unicoq=1.6-8.16-1 paramcoq=1.1.3+coq8.16-1 coq-hott=8.16-1 coq-equations=1.3-8.16-1 coq-gappa=1.5.2-4 coq-hierarchy-builder=1.3.0-2 coq-mtac2=1.4+8.16-1 coq-simple-io=1.7.0-3 coq-corn=8.16.0-1 coq-quickchick=1.6.4-2 mathcomp-analysis=0.5.3-2' dw coqprime_8.15-1+b1 . ANY . -m 'coq => 8.16.0+dfsg-1' dw coqprime_8.15-1+b1 . ANY . -m 'coq-bignums => 8.16.0-1' nmu coq-record-update_0.3.1-1+b1 . ANY . -m 'Rebuild due to coq=8.16.0+dfsg-1 aac-tactics=8.16.0-1 coq-bignums=8.16.0-1 coq-dpdgraph=1.0+8.16-1 coq-elpi=1.15.5-1 coq-reduction-effects=0.1.4-2 coq-hammer=1.3.2+8.16-1 coq-unicoq=1.6-8.16-1 paramcoq=1.1.3+coq8.16-1 coq-hott=8.16-1 coq-equations=1.3-8.16-1 coq-gappa=1.5.2-4 coq-hierarchy-builder=1.3.0-2 coq-mtac2=1.4+8.16-1 coq-simple-io=1.7.0-3 coq-corn=8.16.0-1 coq-quickchick=1.6.4-2 mathcomp-analysis=0.5.3-2' dw coq-record-update_0.3.1-1+b1 . ANY . -m 'coq => 8.16.0+dfsg-1' nmu coq-reglang_1.1.3-1+b1 . ANY . -m 'Rebuild due to coq=8.16.0+dfsg-1 aac-tactics=8.16.0-1 coq-bignums=8.16.0-1 coq-dpdgraph=1.0+8.16-1 coq-elpi=1.15.5-1 coq-reduction-effects=0.1.4-2 coq-hammer=1.3.2+8.16-1 coq-unicoq=1.6-8.16-1 paramcoq=1.1.3+coq8.16-1 coq-hott=8.16-1 coq-equations=1.3-8.16-1 coq-gappa=1.5.2-4 coq-hierarchy-builder=1.3.0-2 coq-mtac2=1.4+8.16-1 coq-simple-io=1.7.0-3 coq-corn=8.16.0-1 coq-quickchick=1.6.4-2 mathcomp-analysis=0.5.3-2' dw coq-reglang_1.1.3-1+b1 . ANY . -m 'coq => 8.16.0+dfsg-1' nmu coq-stdpp_1.8.0-1 . ANY . -m 'Rebuild due to coq=8.16.0+dfsg-1 aac-tactics=8.16.0-1 coq-bignums=8.16.0-1 coq-dpdgraph=1.0+8.16-1 coq-elpi=1.15.5-1 coq-reduction-effects=0.1.4-2 coq-hammer=1.3.2+8.16-1 coq-unicoq=1.6-8.16-1 paramcoq=1.1.3+coq8.16-1 coq-hott=8.16-1 coq-equations=1.3-8.16-1 coq-gappa=1.5.2-4 coq-hierarchy-builder=1.3.0-2 coq-mtac2=1.4+8.16-1 coq-simple-io=1.7.0-3 coq-corn=8.16.0-1 coq-quickchick=1.6.4-2 mathcomp-analysis=0.5.3-2' dw coq-stdpp_1.8.0-1 . ANY . -m 'coq => 8.16.0+dfsg-1' nmu coquelicot_3.2.0-7 . ANY . -m 'Rebuild due to coq=8.16.0+dfsg-1 aac-tactics=8.16.0-1 coq-bignums=8.16.0-1 coq-dpdgraph=1.0+8.16-1 coq-elpi=1.15.5-1 coq-reduction-effects=0.1.4-2 coq-hammer=1.3.2+8.16-1 coq-unicoq=1.6-8.16-1 paramcoq=1.1.3+coq8.16-1 coq-hott=8.16-1 coq-equations=1.3-8.16-1 coq-gappa=1.5.2-4 coq-hierarchy-builder=1.3.0-2 coq-mtac2=1.4+8.16-1 coq-simple-io=1.7.0-3 coq-corn=8.16.0-1 coq-quickchick=1.6.4-2 mathcomp-analysis=0.5.3-2' dw coquelicot_3.2.0-7 . ANY . -m 'coq => 8.16.0+dfsg-1' nmu coq-unimath_20220816-1 . ANY . -m 'Rebuild due to coq=8.16.0+dfsg-1 aac-tactics=8.16.0-1 coq-bignums=8.16.0-1 coq-dpdgraph=1.0+8.16-1 coq-elpi=1.15.5-1 coq-reduction-effects=0.1.4-2 coq-hammer=1.3.2+8.16-1 coq-unicoq=1.6-8.16-1 paramcoq=1.1.3+coq8.16-1 coq-hott=8.16-1 coq-equations=1.3-8.16-1 coq-gappa=1.5.2-4 coq-hierarchy-builder=1.3.0-2 coq-mtac2=1.4+8.16-1 coq-simple-io=1.7.0-3 coq-corn=8.16.0-1 coq-quickchick=1.6.4-2 mathcomp-analysis=0.5.3-2' dw coq-unimath_20220816-1 . ANY . -m 'coq => 8.16.0+dfsg-1' nmu flocq_4.1.0-2 . ANY . -m 'Rebuild due to coq=8.16.0+dfsg-1 aac-tactics=8.16.0-1 coq-bignums=8.16.0-1 coq-dpdgraph=1.0+8.16-1 coq-elpi=1.15.5-1 coq-reduction-effects=0.1.4-2 coq-hammer=1.3.2+8.16-1 coq-unicoq=1.6-8.16-1 paramcoq=1.1.3+coq8.16-1 coq-hott=8.16-1 coq-equations=1.3-8.16-1 coq-gappa=1.5.2-4 coq-hierarchy-builder=1.3.0-2 coq-mtac2=1.4+8.16-1 coq-simple-io=1.7.0-3 coq-corn=8.16.0-1 coq-quickchick=1.6.4-2 mathcomp-analysis=0.5.3-2' dw flocq_4.1.0-2 . ANY . -m 'coq => 8.16.0+dfsg-1' nmu mathcomp-algebra-tactics_1.0.0-6+b1 . ANY . -m 'Rebuild due to coq=8.16.0+dfsg-1 aac-tactics=8.16.0-1 coq-bignums=8.16.0-1 coq-dpdgraph=1.0+8.16-1 coq-elpi=1.15.5-1 coq-reduction-effects=0.1.4-2 coq-hammer=1.3.2+8.16-1 coq-unicoq=1.6-8.16-1 paramcoq=1.1.3+coq8.16-1 coq-hott=8.16-1 coq-equations=1.3-8.16-1 coq-gappa=1.5.2-4 coq-hierarchy-builder=1.3.0-2 coq-mtac2=1.4+8.16-1 coq-simple-io=1.7.0-3 coq-corn=8.16.0-1 coq-quickchick=1.6.4-2 mathcomp-analysis=0.5.3-2' dw mathcomp-algebra-tactics_1.0.0-6+b1 . ANY . -m 'coq => 8.16.0+dfsg-1' dw mathcomp-algebra-tactics_1.0.0-6+b1 . ANY . -m 'coq-elpi => 1.15.5-1' nmu mathcomp-bigenough_1.0.1-8 . ANY . -m 'Rebuild due to coq=8.16.0+dfsg-1 aac-tactics=8.16.0-1 coq-bignums=8.16.0-1 coq-dpdgraph=1.0+8.16-1 coq-elpi=1.15.5-1 coq-reduction-effects=0.1.4-2 coq-hammer=1.3.2+8.16-1 coq-unicoq=1.6-8.16-1 paramcoq=1.1.3+coq8.16-1 coq-hott=8.16-1 coq-equations=1.3-8.16-1 coq-gappa=1.5.2-4 coq-hierarchy-builder=1.3.0-2 coq-mtac2=1.4+8.16-1 coq-simple-io=1.7.0-3 coq-corn=8.16.0-1 coq-quickchick=1.6.4-2 mathcomp-analysis=0.5.3-2' dw mathcomp-bigenough_1.0.1-8 . ANY . -m 'coq => 8.16.0+dfsg-1' nmu mathcomp-finmap_1.5.2-1 . ANY . -m 'Rebuild due to coq=8.16.0+dfsg-1 aac-tactics=8.16.0-1 coq-bignums=8.16.0-1 coq-dpdgraph=1.0+8.16-1 coq-elpi=1.15.5-1 coq-reduction-effects=0.1.4-2 coq-hammer=1.3.2+8.16-1 coq-unicoq=1.6-8.16-1 paramcoq=1.1.3+coq8.16-1 coq-hott=8.16-1 coq-equations=1.3-8.16-1 coq-gappa=1.5.2-4 coq-hierarchy-builder=1.3.0-2 coq-mtac2=1.4+8.16-1 coq-simple-io=1.7.0-3 coq-corn=8.16.0-1 coq-quickchick=1.6.4-2 mathcomp-analysis=0.5.3-2' dw mathcomp-finmap_1.5.2-1 . ANY . -m 'coq => 8.16.0+dfsg-1' nmu mathcomp-multinomials_1.5.5-8+b1 . ANY . -m 'Rebuild due to coq=8.16.0+dfsg-1 aac-tactics=8.16.0-1 coq-bignums=8.16.0-1 coq-dpdgraph=1.0+8.16-1 coq-elpi=1.15.5-1 coq-reduction-effects=0.1.4-2 coq-hammer=1.3.2+8.16-1 coq-unicoq=1.6-8.16-1 paramcoq=1.1.3+coq8.16-1 coq-hott=8.16-1 coq-equations=1.3-8.16-1 coq-gappa=1.5.2-4 coq-hierarchy-builder=1.3.0-2 coq-mtac2=1.4+8.16-1 coq-simple-io=1.7.0-3 coq-corn=8.16.0-1 coq-quickchick=1.6.4-2 mathcomp-analysis=0.5.3-2' dw mathcomp-multinomials_1.5.5-8+b1 . ANY . -m 'coq => 8.16.0+dfsg-1' dw mathcomp-multinomials_1.5.5-8+b1 . ANY . -m 'mathcomp-finmap => 1.5.2-1+b1' dw mathcomp-multinomials_1.5.5-8+b1 . ANY . -m 'mathcomp-bigenough => 1.0.1-8+b1' nmu mathcomp-real-closed_1.1.3-1 . ANY . -m 'Rebuild due to coq=8.16.0+dfsg-1 aac-tactics=8.16.0-1 coq-bignums=8.16.0-1 coq-dpdgraph=1.0+8.16-1 coq-elpi=1.15.5-1 coq-reduction-effects=0.1.4-2 coq-hammer=1.3.2+8.16-1 coq-unicoq=1.6-8.16-1 paramcoq=1.1.3+coq8.16-1 coq-hott=8.16-1 coq-equations=1.3-8.16-1 coq-gappa=1.5.2-4 coq-hierarchy-builder=1.3.0-2 coq-mtac2=1.4+8.16-1 coq-simple-io=1.7.0-3 coq-corn=8.16.0-1 coq-quickchick=1.6.4-2 mathcomp-analysis=0.5.3-2' dw mathcomp-real-closed_1.1.3-1 . ANY . -m 'coq => 8.16.0+dfsg-1' dw mathcomp-real-closed_1.1.3-1 . ANY . -m 'mathcomp-bigenough => 1.0.1-8+b1' nmu mathcomp-zify_1.2.0+1.12+8.13-6 . ANY . -m 'Rebuild due to coq=8.16.0+dfsg-1 aac-tactics=8.16.0-1 coq-bignums=8.16.0-1 coq-dpdgraph=1.0+8.16-1 coq-elpi=1.15.5-1 coq-reduction-effects=0.1.4-2 coq-hammer=1.3.2+8.16-1 coq-unicoq=1.6-8.16-1 paramcoq=1.1.3+coq8.16-1 coq-hott=8.16-1 coq-equations=1.3-8.16-1 coq-gappa=1.5.2-4 coq-hierarchy-builder=1.3.0-2 coq-mtac2=1.4+8.16-1 coq-simple-io=1.7.0-3 coq-corn=8.16.0-1 coq-quickchick=1.6.4-2 mathcomp-analysis=0.5.3-2' dw mathcomp-zify_1.2.0+1.12+8.13-6 . ANY . -m 'coq => 8.16.0+dfsg-1' nmu ott_0.32+ds-2+b1 . ANY . -m 'Rebuild due to coq=8.16.0+dfsg-1 aac-tactics=8.16.0-1 coq-bignums=8.16.0-1 coq-dpdgraph=1.0+8.16-1 coq-elpi=1.15.5-1 coq-reduction-effects=0.1.4-2 coq-hammer=1.3.2+8.16-1 coq-unicoq=1.6-8.16-1 paramcoq=1.1.3+coq8.16-1 coq-hott=8.16-1 coq-equations=1.3-8.16-1 coq-gappa=1.5.2-4 coq-hierarchy-builder=1.3.0-2 coq-mtac2=1.4+8.16-1 coq-simple-io=1.7.0-3 coq-corn=8.16.0-1 coq-quickchick=1.6.4-2 mathcomp-analysis=0.5.3-2' dw ott_0.32+ds-2+b1 . ANY . -m 'coq => 8.16.0+dfsg-1' nmu ssreflect_1.15.0-1 . ANY . -m 'Rebuild due to coq=8.16.0+dfsg-1 aac-tactics=8.16.0-1 coq-bignums=8.16.0-1 coq-dpdgraph=1.0+8.16-1 coq-elpi=1.15.5-1 coq-reduction-effects=0.1.4-2 coq-hammer=1.3.2+8.16-1 coq-unicoq=1.6-8.16-1 paramcoq=1.1.3+coq8.16-1 coq-hott=8.16-1 coq-equations=1.3-8.16-1 coq-gappa=1.5.2-4 coq-hierarchy-builder=1.3.0-2 coq-mtac2=1.4+8.16-1 coq-simple-io=1.7.0-3 coq-corn=8.16.0-1 coq-quickchick=1.6.4-2 mathcomp-analysis=0.5.3-2' dw ssreflect_1.15.0-1 . ANY . -m 'coq => 8.16.0+dfsg-1'