Hi,

I tried to ask on debian-release because it seemed more sensible but
didn't get feedback. [1]

The Coq-related packages have a habit of breaking their ABI with almost
each upload, and until recently that meant broken user configurations: installed packages stopped working because of an upgraded package down
the dependency line.

A few weeks ago, I wrote dh-coq. Basically, the idea is that the
src:coq-foo package builds a binary libcoq-foo package, which declares
it provides a libcoq-foo-1984az package, and when src:coq-bar builds libcoq-bar, dh-coq makes it depend on libcoq-foo-1984az. When the next
upload provides libcoq-foo-d04ab7, apt won't install it because it
would break libcoq-bar: that finer-grained Depends/Provides
organisation means user systems don't get broken. I migrated all Coq-
related packages to this.

Now I took care of user comfort comes the time for mine: I need to
handle transitions correctly.

I have a little script that tells me the following packages needs to be
rebuilt when a transition has to be done ; for example:

$ ./planif_transition.py mathcomp-finmap
mathcomp-finmap
mathcomp-analysis mathcomp-multinomials
coqeal

(the lines are meaningful: same line means parallel build is possible)

So far, so good. But managing transitions is pretty annoying:

(1) The checksums are arch-dependent, which is annoying to write ben
transition scripts. I just need to trigger builds in the right order.
How do I tackle it?

(2) The other C-style lib* packages don't need maintainers to write transitions: the automatic ones just work. How can I have libcoq-*
packages work like this?

Cheers,

J.Puydt

[1] https://lists.debian.org/debian-release/2022/07/msg00373.html

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

Le dimanche 31 juillet 2022 à 12:43 +0200, Sebastian Ramacher a écrit :

On 2022-07-31 12:33:35 +0200, julien.puydt@gmail.com wrote:

Hi,

I tried to ask on debian-release because it seemed more sensible
but
didn't get feedback. [1]

Please file a transition bug. The mailing list has a high volume and
non-bug mails may be overlooked.

Well, I would file a bug for a specific transition, but first I would
like to discuss how to handle transitions for Coq-related packages in
general.

Cheers,

J.Puydt

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

On 2022-07-31 12:33:35 +0200, julien.puydt@gmail.com wrote:

Hi,

I tried to ask on debian-release because it seemed more sensible but
didn't get feedback. [1]

Please file a transition bug. The mailing list has a high volume and
non-bug mails may be overlooked.

Cheers

The Coq-related packages have a habit of breaking their ABI with almost
each upload, and until recently that meant broken user configurations: installed packages stopped working because of an upgraded package down
the dependency line.

A few weeks ago, I wrote dh-coq. Basically, the idea is that the
src:coq-foo package builds a binary libcoq-foo package, which declares
it provides a libcoq-foo-1984az package, and when src:coq-bar builds libcoq-bar, dh-coq makes it depend on libcoq-foo-1984az. When the next
upload provides libcoq-foo-d04ab7, apt won't install it because it
would break libcoq-bar: that finer-grained Depends/Provides
organisation means user systems don't get broken. I migrated all Coq-
related packages to this.

Now I took care of user comfort comes the time for mine: I need to
handle transitions correctly.

I have a little script that tells me the following packages needs to be rebuilt when a transition has to be done ; for example:

$ ./planif_transition.py mathcomp-finmap
mathcomp-finmap
mathcomp-analysis mathcomp-multinomials
coqeal

(the lines are meaningful: same line means parallel build is possible)

So far, so good. But managing transitions is pretty annoying:

(1) The checksums are arch-dependent, which is annoying to write ben transition scripts. I just need to trigger builds in the right order.
How do I tackle it?

(2) The other C-style lib* packages don't need maintainers to write transitions: the automatic ones just work. How can I have libcoq-*
packages work like this?

Cheers,

J.Puydt

[1] https://lists.debian.org/debian-release/2022/07/msg00373.html

--
Sebastian Ramacher

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

Hi,

Am Sonntag, dem 31.07.2022 um 12:33 +0200 schrieb
julien.puydt@gmail.com:

I have a little script that tells me the following packages needs to be rebuilt when a transition has to be done ; for example:

$ ./planif_transition.py mathcomp-finmap
mathcomp-finmap
mathcomp-analysis mathcomp-multinomials
coqeal

(the lines are meaningful: same line means parallel build is possible)

So far, so good. But managing transitions is pretty annoying:

(1) The checksums are arch-dependent, which is annoying to write ben transition scripts. I just need to trigger builds in the right order.
How do I tackle it?

(2) The other C-style lib* packages don't need maintainers to write transitions: the automatic ones just work. How can I have libcoq-*
packages work like this?

it looks like you re-created the setup that the Haskell and Ocaml
packages use, with the provides/depends and hashes.

We have a tool that produces a file with the necessary commands to pass
to wanna-build, see for example in https://people.debian.org/~iliastsi/binNMUs-haskell.txt

I used to produce a file like this for Ocaml, but it’s gone since I
disabled my account. It’s configured via a simple regex, libghc-(.*)-dev-([0-9.]+)-([0-9a-f]{5})
in the case of Ocaml.

The source code is at https://salsa.debian.org/haskell-team/tools/-/tree/master/binnmus

It may be useful to you too

Cheers,
Joachim


--
Joachim “nomeata” Breitner • nomeata@debian.org • https://j.oach.im/  

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

On Sun, Jul 31, 2022 at 01:00:03PM +0200, julien.puydt@gmail.com wrote:

Please file a transition bug. The mailing list has a high volume and non-bug mails may be overlooked.

Well, I would file a bug for a specific transition, but first I would
like to discuss how to handle transitions for Coq-related packages in general.

file a general bug against release.debian.org then. The mailing list has a
high volume and non-bug mails may be overlooked. ;)


--
cheers,
Holger

⢀⣴⠾⠻⢶⣦⠀
⣾⠁⢠⠒⠀⣿⡁ holger@(debian|reproducible-builds|layer-acht).org
⢿⡄⠘⠷⠚⠋⠀ OpenPGP: B8BF54137B09D35CF026FE9D 091AB856069AAA1C
⠈⠳⣄

If you upload your address book to "the cloud", I don't want to be in it.

-----BEGIN PGP SIGNATURE-----

iQIzBAABCgAdFiEEuL9UE3sJ01zwJv6dCRq4VgaaqhwFAmLo8ZcACgkQCRq4Vgaa qhy3XA//eTj0catxgQFRMlLt+2xJeSuDf8aZD4+CQB3IZWOmwDgeJGxW8eqEZanC KzxbMLK+9mYJggboZAbWl0QTxYRyZp+TugLJLEosH8EYs0XpRVKcI7agkl0oAHMf 4PukgT8lHFfHrMXzQetqMcutBYG8zgTBoDQxZbHk0HyEnbMElGO4CttftBFm3Ry9 oxdrcy/B238/+R28XIT7Nxolpx8yEotL2FQty4dH1zVzvdqC84MYna8Sqs7s1dbU WoWfl9KeoR6lccXnrOl3CzlbfXjSIlcmiP4WLzjRWvCQYiCQtpRiYnqkksFi3NUh BccBl2UePV2RIGOanBL6bEo+3Pg1KbndfM7RzNpawgdw4TN+BvHJwrMdiXWCw7aP iaAB8qVZRhU4NkavzxNB06tJoBCUbr0+Hev9k1iRQtnl38/QLPaP1d3Fv2FfhyoR 7Wdh0cpYeqlqbKrUNEm/MubUAFx8axDBjmGMs7cuYLKC+Mmpd5t9SiEOPTcHEFli QX2V/C6WHsDJ/Jc5amo4tw8hRngnTxcI8yL6ZYQTbQE19FV2nU7Xh7EhDLl6b2zJ 3+E+hG8VWEkrYzwk8jjkctuZnXKdnid0ETNhCz+

Le dimanche 31 juillet 2022 à 12:43 +0200, Sebastian Ramacher a écrit :

On 2022-07-31 12:33:35 +0200, julien.puydt@gmail.com wrote:

Hi,

I tried to ask on debian-release because it seemed more sensible
but didn't get feedback. [1]

Please file a transition bug. The mailing list has a high volume and
non-bug mails may be overlooked.

Bug 1016416, but that doesn't look that efficient.

J.Puydt

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

Hi,

Le lundi 01 août 2022 à 14:20 +0200, Joachim Breitner a écrit :

it looks like you re-created the setup that the Haskell and Ocaml
packages use, with the provides/depends and hashes.

Yes, dh-ocaml was a great help. I learned Perl to write dh-coq...

We have a tool that produces a file with the necessary commands to
pass to wanna-build, see for example in https://people.debian.org/~iliastsi/binNMUs-haskell.txt

I used to produce a file like this for Ocaml, but it’s gone since I disabled my account. It’s configured via a simple regex, libghc-(.*)-dev-([0-9.]+)-([0-9a-f]{5})
in the case of Ocaml.

The source code is at https://salsa.debian.org/haskell-team/tools/-/tree/master/binnmus

It may be useful to you too

The source code is very complex, and it looks like it can get the
hashes of the new packages -- something I'm incapable of doing! Indeed
that would mean building the whole stack on all architectures so the computations happen. Indeed the hashes I have are arch-dependent...

I tried to write a simpler version, which might still be valuable ;
here is the wanna-build script I would get if I wanted to upload coq-
elpi 1.15.5-1 to unstable:

./wanna-build.py coq-elpi 1.15.5-1

nmu coq-hierarchy-builder_1.3.0-1 . ANY . -m 'Rebuild due to new coq-
elpi 1.15.5-1'
dw coq-hierarchy-builder_1.3.0-1 . ANY . -m 'coq-elpi => 1.15.5-1'
nmu mathcomp-algebra-tactics_1.0.0-6+b1 . ANY . -m 'Rebuild due to new coq-elpi 1.15.5-1'
dw mathcomp-algebra-tactics_1.0.0-6+b1 . ANY . -m 'coq-elpi => 1.15.5-
1'
nmu mathcomp-analysis_0.5.2-2 . ANY . -m 'Rebuild due to new coq-elpi 1.15.5-1'
dw mathcomp-analysis_0.5.2-2 . ANY . -m 'coq-elpi => 1.15.5-1'
dw mathcomp-analysis_0.5.2-2 . ANY . -m 'coq-hierarchy-builder =>
1.3.0-1+b1'

does that look correct?

How are automatic transitions generated? It would probably be much more efficient if I could provide scripts to automatically provide
transition scripts such as above: they would only need to change when
the list of Coq-related packages changes.

Cheers,

J.Puydt

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)