Bug#1087631: Transition: coq 8.20

[Julien Puydt]

Package: release.debian.org
Severity: normal
User: ***@packages.debian.org
Usertags: transition
X-Debbugs-CC: debian-ocaml-***@lists.debian.org

Coq version 8.20 has been out since the beginning of september. I
prepared a coherent set of versions for the whole Coq-in-Debian set of
packages (45 packages).

I need a transition slot before I upload anything.

Cheers,

J.Puydt

PS: the relevant transition script is :

dw aac-tactics_8.20.0-1 . ANY . -m 'coq >= 8.20.0-1'
dw coq-dpdgraph_1.0+8.20-1 . ANY . -m 'coq >= 8.20.0-1'
dw coq-elpi_2.2.3-1 . ANY . -m 'coq >= 8.20.0-1'
dw coq-elpi_2.2.3-1 . ANY . -m 'elpi >= 1.19.6-1'
dw coq-ext-lib_0.12.2-1 . ANY . -m 'coq >= 8.20.0-1'
dw coq-hammer_1.3.2+8.20-1 . ANY . -m 'coq >= 8.20.0-1'
dw coq-hott_8.20-1 . ANY . -m 'coq >= 8.20.0-1'
dw coq-menhirlib_20240715+ds-1 . ANY . -m 'coq >= 8.20.0-1'
dw coq-serapi_8.20.0+0.20.0-1 . ANY . -m 'coq >= 8.20.0-1'
dw coq-stdpp_1.11.0-1 . ANY . -m 'coq >= 8.20.0-1'
dw coq-unicoq_1.6-8.19-3 . ANY . -m 'coq >= 8.20.0-1'
dw coq-unimath_20240923-1 . ANY . -m 'coq >= 8.20.0-1'
dw flocq_4.2.0-1 . ANY . -m 'coq >= 8.20.0-1'
dw paramcoq_1.1.3+coq8.20 . ANY . -m 'coq >= 8.20.0-1'
nmu coq-bignums_9.0.0+coq8.20-1+b5 . ANY . -m 'Rebuild because of
upload of coq=8.20.0-1'
dw coq-bignums_9.0.0+coq8.20-1+b5 . ANY . -m 'coq >= 8.20.0-1'
nmu coq-libhyps_2.0.8-4+b4 . ANY . -m 'Rebuild because of upload of
coq=8.20.0-1'
dw coq-libhyps_2.0.8-4+b4 . ANY . -m 'coq >= 8.20.0-1'
nmu coq-record-update_0.3.4-3+b4 . ANY . -m 'Rebuild because of upload
of coq=8.20.0-1'
dw coq-record-update_0.3.4-3+b4 . ANY . -m 'coq >= 8.20.0-1'
nmu coq-reduction-effects_0.1.5-5+b4 . ANY . -m 'Rebuild because of
upload of coq=8.20.0-1'
dw coq-reduction-effects_0.1.5-5+b4 . ANY . -m 'coq >= 8.20.0-1'
nmu ott_0.33+ds-4+b4 . ANY . -m 'Rebuild because of upload of
coq=8.20.0-1'
dw ott_0.33+ds-4+b4 . ANY . -m 'coq >= 8.20.0-1'
dw coq-equations_1.3.1-8.20-1 . ANY . -m 'coq-hott >= 8.20-1'
dw coq-equations_1.3.1-8.20-1 . ANY . -m 'coq >= 8.20.0-1'
dw coq-iris_4.3.0-1 . ANY . -m 'coq >= 8.20.0-1'
dw coq-iris_4.3.0-1 . ANY . -m 'coq-stdpp >= 1.11.0-1'
dw coq-mtac2_1.40+8.19-3 . ANY . -m 'coq-unicoq >= 1.6-8.19-3'
dw coq-mtac2_1.40+8.19-3 . ANY . -m 'coq >= 8.20.0-1'
dw coq-simple-io_1.10.0-1 . ANY . -m 'coq-ext-lib >= 0.12.2-1'
dw coq-simple-io_1.10.0-1 . ANY . -m 'coq >= 8.20.0-1'
nmu coq-gappa_1.5.5-2+b4 . ANY . -m 'Rebuild because of upload of
flocq=4.2.0-1 coq=8.20.0-1'
dw coq-gappa_1.5.5-2+b4 . ANY . -m 'flocq >= 4.2.0-1'
dw coq-gappa_1.5.5-2+b4 . ANY . -m 'coq >= 8.20.0-1'
nmu coq-hierarchy-builder_1.7.0-2+b10 . ANY . -m 'Rebuild because of
upload of coq=8.20.0-1 coq-elpi=2.2.3-1'
dw coq-hierarchy-builder_1.7.0-2+b10 . ANY . -m 'coq >= 8.20.0-1'
dw coq-hierarchy-builder_1.7.0-2+b10 . ANY . -m 'coq-elpi >= 2.2.3-1'
nmu coq-math-classes_8.19.0-1+b7 . ANY . -m 'Rebuild because of upload
of coq-bignums=9.0.0+coq8.20-1+b5 coq=8.20.0-1'
dw coq-math-classes_8.19.0-1+b7 . ANY . -m 'coq-bignums >=
9.0.0+coq8.20-1+b5'
dw coq-math-classes_8.19.0-1+b7 . ANY . -m 'coq >= 8.20.0-1'
nmu coqprime_8.19-2+b4 . ANY . -m 'Rebuild because of upload of coq-
bignums=9.0.0+coq8.20-1+b5 coq=8.20.0-1'
dw coqprime_8.19-2+b4 . ANY . -m 'coq-bignums >= 9.0.0+coq8.20-1+b5'
dw coqprime_8.19-2+b4 . ANY . -m 'coq >= 8.20.0-1'
dw coq-corn_8.19.0+ds1-2 . ANY . -m 'coq-bignums >= 9.0.0+coq8.20-
1+b5'
dw coq-corn_8.19.0+ds1-2 . ANY . -m 'coq >= 8.20.0-1'
dw coq-corn_8.19.0+ds1-2 . ANY . -m 'coq-math-classes >= 8.19.0-1+b7'
nmu ssreflect_2.2.0-2+b9 . ANY . -m 'Rebuild because of upload of coq-
hierarchy-builder=1.7.0-2+b10 coq=8.20.0-1'
dw ssreflect_2.2.0-2+b9 . ANY . -m 'coq-hierarchy-builder >= 1.7.0-
2+b10'
dw ssreflect_2.2.0-2+b9 . ANY . -m 'coq >= 8.20.0-1'
dw coq-relation-algebra_1.7.11-1 . ANY . -m 'aac-tactics >= 8.20.0-1'
dw coq-relation-algebra_1.7.11-1 . ANY . -m 'coq >= 8.20.0-1'
dw coq-relation-algebra_1.7.11-1 . ANY . -m 'ssreflect >= 2.2.0-2+b9'
dw coquelicot_3.4.2-1 . ANY . -m 'coq >= 8.20.0-1'
dw coquelicot_3.4.2-1 . ANY . -m 'ssreflect >= 2.2.0-2+b9'
dw coq-quickchick_2.0.4-1 . ANY . -m 'coq-simple-io >= 1.10.0-1'
dw coq-quickchick_2.0.4-1 . ANY . -m 'coq-ext-lib >= 0.12.2-1'
dw coq-quickchick_2.0.4-1 . ANY . -m 'coq >= 8.20.0-1'
dw coq-quickchick_2.0.4-1 . ANY . -m 'ssreflect >= 2.2.0-2+b9'
nmu coq-deriving_0.2.0-3+b7 . ANY . -m 'Rebuild because of upload of
coq=8.20.0-1 ssreflect=2.2.0-2+b9'
dw coq-deriving_0.2.0-3+b7 . ANY . -m 'coq >= 8.20.0-1'
dw coq-deriving_0.2.0-3+b7 . ANY . -m 'ssreflect >= 2.2.0-2+b9'
nmu coq-reglang_1.2.1-4+b7 . ANY . -m 'Rebuild because of upload of
coq=8.20.0-1 ssreflect=2.2.0-2+b9'
dw coq-reglang_1.2.1-4+b7 . ANY . -m 'coq >= 8.20.0-1'
dw coq-reglang_1.2.1-4+b7 . ANY . -m 'ssreflect >= 2.2.0-2+b9'
nmu mathcomp-bigenough_1.0.1-14+b7 . ANY . -m 'Rebuild because of
upload of coq=8.20.0-1 ssreflect=2.2.0-2+b9'
dw mathcomp-bigenough_1.0.1-14+b7 . ANY . -m 'coq >= 8.20.0-1'
dw mathcomp-bigenough_1.0.1-14+b7 . ANY . -m 'ssreflect >= 2.2.0-2+b9'
nmu mathcomp-finmap_2.1.0-2+b7 . ANY . -m 'Rebuild because of upload
of coq=8.20.0-1 ssreflect=2.2.0-2+b9'
dw mathcomp-finmap_2.1.0-2+b7 . ANY . -m 'coq >= 8.20.0-1'
dw mathcomp-finmap_2.1.0-2+b7 . ANY . -m 'ssreflect >= 2.2.0-2+b9'
nmu mathcomp-zify_1.5.0+2.0+8.16-3+b7 . ANY . -m 'Rebuild because of
upload of coq=8.20.0-1 ssreflect=2.2.0-2+b9'
dw mathcomp-zify_1.5.0+2.0+8.16-3+b7 . ANY . -m 'coq >= 8.20.0-1'
dw mathcomp-zify_1.5.0+2.0+8.16-3+b7 . ANY . -m 'ssreflect >= 2.2.0-
2+b9'
dw coq-interval_4.11.1-1 . ANY . -m 'coq >= 8.20.0-1'
dw coq-interval_4.11.1-1 . ANY . -m 'coq-bignums >= 9.0.0+coq8.20-
1+b5'
dw coq-interval_4.11.1-1 . ANY . -m 'flocq >= 4.2.0-1'
dw coq-interval_4.11.1-1 . ANY . -m 'coquelicot >= 3.4.2-1'
dw coq-interval_4.11.1-1 . ANY . -m 'ssreflect >= 2.2.0-2+b9'
dw mathcomp-analysis_1.6.0-1 . ANY . -m 'coq >= 8.20.0-1'
dw mathcomp-analysis_1.6.0-1 . ANY . -m 'mathcomp-finmap >= 2.1.0-
2+b7'
dw mathcomp-analysis_1.6.0-1 . ANY . -m 'mathcomp-bigenough >= 1.0.1-
14+b7'
dw mathcomp-analysis_1.6.0-1 . ANY . -m 'ssreflect >= 2.2.0-2+b9'
dw mathcomp-analysis_1.6.0-1 . ANY . -m 'coq-hierarchy-builder >=
1.7.0-2+b10'
dw mathcomp-analysis_1.6.0-1 . ANY . -m 'coq-elpi >= 2.2.3-1'
dw mathcomp-multinomials_2.2.0-4 . ANY . -m 'mathcomp-finmap >= 2.1.0-
2+b7'
dw mathcomp-multinomials_2.2.0-4 . ANY . -m 'mathcomp-bigenough >=
1.0.1-14+b7'
dw mathcomp-multinomials_2.2.0-4 . ANY . -m 'coq >= 8.20.0-1'
dw mathcomp-multinomials_2.2.0-4 . ANY . -m 'ssreflect >= 2.2.0-2+b9'
dw mathcomp-real-closed_2.0.1-1 . ANY . -m 'mathcomp-bigenough >=
1.0.1-14+b7'
dw mathcomp-real-closed_2.0.1-1 . ANY . -m 'coq >= 8.20.0-1'
dw mathcomp-real-closed_2.0.1-1 . ANY . -m 'ssreflect >= 2.2.0-2+b9'
nmu coq-extructures_0.4.0-4+b7 . ANY . -m 'Rebuild because of upload
of coq-deriving=0.2.0-3+b7 coq=8.20.0-1 ssreflect=2.2.0-2+b9'
dw coq-extructures_0.4.0-4+b7 . ANY . -m 'coq-deriving >= 0.2.0-3+b7'
dw coq-extructures_0.4.0-4+b7 . ANY . -m 'coq >= 8.20.0-1'
dw coq-extructures_0.4.0-4+b7 . ANY . -m 'ssreflect >= 2.2.0-2+b9'
nmu mathcomp-algebra-tactics_1.2.3-4+b7 . ANY . -m 'Rebuild because of
upload of mathcomp-zify=1.5.0+2.0+8.16-3+b7 coq=8.20.0-1 coq-
elpi=2.2.3-1 ssreflect=2.2.0-2+b9'
dw mathcomp-algebra-tactics_1.2.3-4+b7 . ANY . -m 'mathcomp-zify >=
1.5.0+2.0+8.16-3+b7'
dw mathcomp-algebra-tactics_1.2.3-4+b7 . ANY . -m 'coq >= 8.20.0-1'
dw mathcomp-algebra-tactics_1.2.3-4+b7 . ANY . -m 'coq-elpi >= 2.2.3-
1'
dw mathcomp-algebra-tactics_1.2.3-4+b7 . ANY . -m 'ssreflect >= 2.2.0-
2+b9'
nmu coqeal_2.0.2-2+b7 . ANY . -m 'Rebuild because of upload of
coq=8.20.0-1 coq-bignums=9.0.0+coq8.20-1+b5 ssreflect=2.2.0-2+b9
paramcoq=1.1.3+coq8.20 mathcomp-real-closed=2.0.1-1'
dw coqeal_2.0.2-2+b7 . ANY . -m 'coq >= 8.20.0-1'
dw coqeal_2.0.2-2+b7 . ANY . -m 'coq-bignums >= 9.0.0+coq8.20-1+b5'
dw coqeal_2.0.2-2+b7 . ANY . -m 'ssreflect >= 2.2.0-2+b9'
dw coqeal_2.0.2-2+b7 . ANY . -m 'paramcoq >= 1.1.3+coq8.20'
dw coqeal_2.0.2-2+b7 . ANY . -m 'mathcomp-real-closed >= 2.0.1-1'

[Julien Puydt]

Hi

Post by Julien Puydt
Package: release.debian.org
Severity: normal
Usertags: transition
Coq version 8.20 has been out since the beginning of september. I
prepared a coherent set of versions for the whole Coq-in-Debian set of
packages (45 packages).
I need a transition slot before I upload anything.

Have you done any local rebuilds to ensure that packages build fine
against the
new coq version?

Yes, that is what I meant when I wrote I prepared a coherent set ; sorry if
I wasn't clear.

Thanks,

JP

[Debian Bug Tracking System]

tags -1 confirmed

Bug #1087631 [release.debian.org] Transition: coq 8.20
Added tag(s) confirmed.

[Debian Bug Tracking System]

Your message dated Sat, 04 Jan 2025 12:36:48 +0100
with message-id <***@gmail.com>
and subject line Done transition
has caused the Debian Bug report #1087631,
regarding Transition: coq 8.20
to be marked as done.

This means that you claim that the problem has been dealt with.
If this is not the case it is now your responsibility to reopen the
Bug report if necessary, and/or fix the problem forthwith.

(NB: If you are a system administrator and have no idea what this
message is talking about, this may indicate a serious mail system
misconfiguration somewhere. Please contact ***@bugs.debian.org
immediately.)

[Debian Bug Tracking System]

Your message dated Sat, 04 Jan 2025 12:36:48 +0100
with message-id <***@gmail.com>
and subject line Done transition
has caused the Debian Bug report #1090727,
regarding transition: elpi
to be marked as done.

This means that you claim that the problem has been dealt with.
If this is not the case it is now your responsibility to reopen the
Bug report if necessary, and/or fix the problem forthwith.

(NB: If you are a system administrator and have no idea what this
message is talking about, this may indicate a serious mail system
misconfiguration somewhere. Please contact ***@bugs.debian.org
immediately.)