Control: tags -1 confirmed On 2022-09-06 07:14:25 +0200, Julien Puydt wrote: > 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!",
Please go ahead and let me know once you're done with all the uploads. Cheers > > 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' -- Sebastian Ramacher
