#1061476 transition: elpi

Package:
release.debian.org
Source:
release.debian.org
Submitter:
Date:
2024-02-24 07:42:04 UTC
Severity:
normal
#1061476#5
Date:
2024-01-25 05:22:23 UTC
From:
To:
there is a new upstream for elpi in the OCaml packages, which has an
impact on a few Coq packages.

I checked locally (using sbuild in a chroot) everything could move
fine.

Several packages need a new version and then some need just a rebuild.
A ben description of the plan is in post scriptum.

Waiting for your ACK to upload the new packages sources.

Thanks,

J.Puydt

PS:
 dw coq-elpi 2.0.0-1 . ANY . -m 'elpi >= 1.18.1-1'
 dw coq-hierarchy-builder_1.7.0-1 . ANY . -m 'coq-elpi >= 2.0.0-1'
 dw ssreflect_2.2.0-1 . ANY . -m 'coq-hierarchy-builder >= 1.7.0-1'
 dw coq-relation-algebra_1.7.10-1 . ANY . -m 'ssreflect >= 2.2.0-1'
 dw mathcomp-finmap_2.1.0-1 . ANY . -m 'ssreflect >= 2.2.0-1'
 nmu coq-deriving_0.2.0-1+b1 . ANY . -m 'Rebuild because of upload of
ssreflect=2.2.0-1'
 dw coq-deriving_0.2.0-1+b1 . ANY . -m 'ssreflect >= 2.2.0-1'
 nmu coq-reglang_1.2.1-1+b1 . ANY . -m 'Rebuild because of upload of
ssreflect=2.2.0-1'
 dw coq-reglang_1.2.1-1+b1 . ANY . -m 'ssreflect >= 2.2.0-1'
 nmu coquelicot_3.4.1-1+b1 . ANY . -m 'Rebuild because of upload of
ssreflect=2.2.0-1'
 dw coquelicot_3.4.1-1+b1 . ANY . -m 'ssreflect >= 2.2.0-1'
 nmu mathcomp-bigenough_1.0.1-12+b1 . ANY . -m 'Rebuild because of
upload of ssreflect=2.2.0-1'
 dw mathcomp-bigenough_1.0.1-12+b1 . ANY . -m 'ssreflect >= 2.2.0-1'
 nmu mathcomp-zify_1.5.0+2.0+8.16-1+b1 . ANY . -m 'Rebuild because of
upload of ssreflect=2.2.0-1'
 dw mathcomp-zify_1.5.0+2.0+8.16-1+b1 . ANY . -m 'ssreflect >= 2.2.0-1'
 nmu coq-quickchick_2.0.2-1+b1 . ANY . -m 'Rebuild because of upload of
ssreflect=2.2.0-1'
 dw coq-quickchick_2.0.2-1+b1 . ANY . -m 'ssreflect >= 2.2.0-1'
 nmu coq-extructures_0.4.0-1+b1 . ANY . -m 'Rebuild because of upload
of ssreflect=2.2.0-1 coq-deriving=0.2.0-1+b1'
 dw coq-extructures_0.4.0-1+b1 . ANY . -m 'ssreflect >= 2.2.0-1'
 dw coq-extructures_0.4.0-1+b1 . ANY . -m 'coq-deriving >= 0.2.0-1+b1'
 nmu coq-interval_4.9.0-1+b2 . ANY . -m 'Rebuild because of upload of
ssreflect=2.2.0-1 coquelicot=3.4.1-1+b1'
 dw coq-interval_4.9.0-1+b2 . ANY . -m 'ssreflect >= 2.2.0-1'
 dw coq-interval_4.9.0-1+b2 . ANY . -m 'coquelicot >= 3.4.1-1+b1'
 nmu mathcomp-algebra-tactics_1.2.3-1+b1 . ANY . -m 'Rebuild because of
upload of ssreflect=2.2.0-1 mathcomp-zify=1.5.0+2.0+8.16-1+b1 coq-
elpi=2.0.0-1'
 dw mathcomp-algebra-tactics_1.2.3-1+b1 . ANY . -m 'ssreflect >= 2.2.0-
1'
 dw mathcomp-algebra-tactics_1.2.3-1+b1 . ANY . -m 'mathcomp-zify >=
1.5.0+2.0+8.16-1+b1'
 dw mathcomp-algebra-tactics_1.2.3-1+b1 . ANY . -m 'coq-elpi >= 2.0.0-
1'
 nmu mathcomp-multinomials_2.2.0-1+b1 . ANY . -m 'Rebuild because of
upload of ssreflect=2.2.0-1 mathcomp-finmap=2.1.0-1 mathcomp-
bigenough=1.0.1-12+b1'
 dw mathcomp-multinomials_2.2.0-1+b1 . ANY . -m 'ssreflect >= 2.2.0-1'
 dw mathcomp-multinomials_2.2.0-1+b1 . ANY . -m 'mathcomp-finmap >=
2.1.0-1'
 dw mathcomp-multinomials_2.2.0-1+b1 . ANY . -m 'mathcomp-bigenough >=
1.0.1-12+b1'
 nmu mathcomp-real-closed_2.0.0-1+b1 . ANY . -m 'Rebuild because of
upload of ssreflect=2.2.0-1 mathcomp-bigenough=1.0.1-12+b1'
 dw mathcomp-real-closed_2.0.0-1+b1 . ANY . -m 'ssreflect >= 2.2.0-1'
 dw mathcomp-real-closed_2.0.0-1+b1 . ANY . -m 'mathcomp-bigenough >=
1.0.1-12+b1'
 nmu coqeal_2.0.1-1+b1 . ANY . -m 'Rebuild because of upload of
mathcomp-real-closed=2.0.0-1+b1 ssreflect=2.2.0-1'
 dw coqeal_2.0.1-1+b1 . ANY . -m 'mathcomp-real-closed >= 2.0.0-1+b1'
 dw coqeal_2.0.1-1+b1 . ANY . -m 'ssreflect >= 2.2.0-1'
#1061476#10
Date:
2024-01-30 10:14:13 UTC
From:
To:
Hi,

someone uploaded a new mathcomp-analysis not knowing about this planned
transition, so it should be taken into account.

Cheers,

J.Puydt

PS: updated ben script

 dw coq-elpi_2.0.0-1 . ANY . -m 'elpi >= 1.18.1-1'
 dw coq-hierarchy-builder_1.7.0-1 . ANY . -m 'coq-elpi >= 2.0.0-1'
 dw ssreflect_2.2.0-1 . ANY . -m 'coq-hierarchy-builder >= 1.7.0-1'
 dw coq-relation-algebra_1.7.10-1 . ANY . -m 'ssreflect >= 2.2.0-1'
 dw mathcomp-finmap_2.1.0-1 . ANY . -m 'ssreflect >= 2.2.0-1'
 nmu coq-deriving_0.2.0-1+b1 . ANY . -m 'Rebuild because of upload of
ssreflect=2.2.0-1'
 dw coq-deriving_0.2.0-1+b1 . ANY . -m 'ssreflect >= 2.2.0-1'
 nmu coq-reglang_1.2.1-1+b1 . ANY . -m 'Rebuild because of upload of
ssreflect=2.2.0-1'
 dw coq-reglang_1.2.1-1+b1 . ANY . -m 'ssreflect >= 2.2.0-1'
 nmu coquelicot_3.4.1-1+b1 . ANY . -m 'Rebuild because of upload of
ssreflect=2.2.0-1'
 dw coquelicot_3.4.1-1+b1 . ANY . -m 'ssreflect >= 2.2.0-1'
 nmu mathcomp-bigenough_1.0.1-12+b1 . ANY . -m 'Rebuild because of
upload of ssreflect=2.2.0-1'
 dw mathcomp-bigenough_1.0.1-12+b1 . ANY . -m 'ssreflect >= 2.2.0-1'
 nmu mathcomp-zify_1.5.0+2.0+8.16-1+b1 . ANY . -m 'Rebuild because of
upload of ssreflect=2.2.0-1'
 dw mathcomp-zify_1.5.0+2.0+8.16-1+b1 . ANY . -m 'ssreflect >= 2.2.0-1'
 nmu coq-quickchick_2.0.2-1+b1 . ANY . -m 'Rebuild because of upload of
ssreflect=2.2.0-1'
 dw coq-quickchick_2.0.2-1+b1 . ANY . -m 'ssreflect >= 2.2.0-1'
 nmu coq-extructures_0.4.0-1+b1 . ANY . -m 'Rebuild because of upload
of ssreflect=2.2.0-1 coq-deriving=0.2.0-1+b1'
 dw coq-extructures_0.4.0-1+b1 . ANY . -m 'ssreflect >= 2.2.0-1'
 dw coq-extructures_0.4.0-1+b1 . ANY . -m 'coq-deriving >= 0.2.0-1+b1'
 nmu coq-interval_4.9.0-1+b2 . ANY . -m 'Rebuild because of upload of
ssreflect=2.2.0-1 coquelicot=3.4.1-1+b1'
 dw coq-interval_4.9.0-1+b2 . ANY . -m 'ssreflect >= 2.2.0-1'
 dw coq-interval_4.9.0-1+b2 . ANY . -m 'coquelicot >= 3.4.1-1+b1'
 nmu mathcomp-algebra-tactics_1.2.3-1+b1 . ANY . -m 'Rebuild because of
upload of mathcomp-zify=1.5.0+2.0+8.16-1+b1 ssreflect=2.2.0-1 coq-
elpi=2.0.0-1'
 dw mathcomp-algebra-tactics_1.2.3-1+b1 . ANY . -m 'mathcomp-zify >=
1.5.0+2.0+8.16-1+b1'
 dw mathcomp-algebra-tactics_1.2.3-1+b1 . ANY . -m 'ssreflect >= 2.2.0-
1'
 dw mathcomp-algebra-tactics_1.2.3-1+b1 . ANY . -m 'coq-elpi >= 2.0.0-
1'
 nmu mathcomp-analysis_1.0.0-1+b1 . ANY . -m 'Rebuild because of upload
of coq-hierarchy-builder=1.7.0-1 coq-elpi=2.0.0-1 mathcomp-
bigenough=1.0.1-12+b1 mathcomp-finmap=2.1.0-1 ssreflect=2.2.0-1'
 dw mathcomp-analysis_1.0.0-1+b1 . ANY . -m 'coq-hierarchy-builder >=
1.7.0-1'
 dw mathcomp-analysis_1.0.0-1+b1 . ANY . -m 'coq-elpi >= 2.0.0-1'
 dw mathcomp-analysis_1.0.0-1+b1 . ANY . -m 'mathcomp-bigenough >=
1.0.1-12+b1'
 dw mathcomp-analysis_1.0.0-1+b1 . ANY . -m 'mathcomp-finmap >= 2.1.0-
1'
 dw mathcomp-analysis_1.0.0-1+b1 . ANY . -m 'ssreflect >= 2.2.0-1'
 nmu mathcomp-multinomials_2.2.0-1+b1 . ANY . -m 'Rebuild because of
upload of mathcomp-bigenough=1.0.1-12+b1 mathcomp-finmap=2.1.0-1
ssreflect=2.2.0-1'
 dw mathcomp-multinomials_2.2.0-1+b1 . ANY . -m 'mathcomp-bigenough >=
1.0.1-12+b1'
 dw mathcomp-multinomials_2.2.0-1+b1 . ANY . -m 'mathcomp-finmap >=
2.1.0-1'
 dw mathcomp-multinomials_2.2.0-1+b1 . ANY . -m 'ssreflect >= 2.2.0-1'
 nmu mathcomp-real-closed_2.0.0-1+b1 . ANY . -m 'Rebuild because of
upload of mathcomp-bigenough=1.0.1-12+b1 ssreflect=2.2.0-1'
 dw mathcomp-real-closed_2.0.0-1+b1 . ANY . -m 'mathcomp-bigenough >=
1.0.1-12+b1'
 dw mathcomp-real-closed_2.0.0-1+b1 . ANY . -m 'ssreflect >= 2.2.0-1'
 nmu coqeal_2.0.1-1+b1 . ANY . -m 'Rebuild because of upload of
mathcomp-real-closed=2.0.0-1+b1 ssreflect=2.2.0-1'
 dw coqeal_2.0.1-1+b1 . ANY . -m 'mathcomp-real-closed >= 2.0.0-1+b1'
 dw coqeal_2.0.1-1+b1 . ANY . -m 'ssreflect >= 2.2.0-1'
#1061476#15
Date:
2024-02-09 09:06:28 UTC
From:
To:
Hi,

is there a particular problem with what I'm proposing? I checked and
didn't see any collision with an ocaml transition or some such.

Thanks,

J.Puydt
#1061476#20
Date:
2024-02-09 09:19:38 UTC
From:
To:
Hi Julien

Until the time_t transition is done, we won't process other transition.
Normal operation will continue after the time_t transition.

Cheers
#1061476#25
Date:
2024-02-09 09:21:50 UTC
From:
To:
Hi,

Le vendredi 09 février 2024 à 10:19 +0100, Sebastian Ramacher a écrit :

Ah, good!

Thanks!

J
#1061476#30
Date:
2024-02-24 07:38:30 UTC
From:
To:
Hi,

I'm already working on the next big transition for the Coq ecosystem in
Debian, and this one will just be part of it.

Cheers,

J.Puydt