Bug#1019239: transition: coq (41 packages involved)

Package: release.debian.org
Severity: normal
User: release.debian.org@packages.debian.org
Usertags: transition

X-Debbugs-Cc: Debian OCaml Maintainers <debian-ocaml-maint@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'