Hi,

I'm trying to get more of the coq ecosystem into Debian. There are
several things I would like to package -- but first I think I need to consolidate what's already there.

Here is a list of issues I have, on which I would need feedback ; I put explicit "Question: ..." to make it clearer what is asked.

(1) Currently, each time coq is rebuilt (either because OCaml was
updated or it was updated itself), the whole stack should be too, or
things just break! (There are some bugs about it: #741535, #977258
[cloned as #979756]).

I expect the new uploads should trigger automatic transitions, much
like soname changes do for C/C++ libs. That makes things much easier.

I know "ben" (https://ben.debian.net/) helps following transitions (here: https://release.debian.org/transitions/), I know https://wiki.debian.org/Teams/ReleaseTeam/Transitions explains how
manual transitions work and mentions an auto-transitioner, but didn't
find where that thing is.

Question: how are such things done? (pointers to code and/or
documentation are welcome)

(2) I'm not sure the current source packages all give good binary
packages (here: content).

The src:coq package provides libcoq-stdlib which contains the coq
standard library and its doc. The binary libcoq-core-ocaml and libcoq- core-ocaml-dev look honest OCaml packages, providing the correct files
in /usr/lib/ocaml/coq-core. Probably ok.

For src:coq-elpi, things don't look so good:
- libcoq-elpi-ocaml is mostly .v, .vo and .glob coq files in /usr/lib/ocaml/coq/user-contrib/elpi, with only a pair of .cma/.cmxs in /usr/lib/ocaml/coq/user-contrib/elpi, so it doesn't look sane.
- libcoq-elpi-ocaml-dev has .a, .cmi, .cmo, .cmx, .cmxa files so I
think it's good.

Question: shouldn't I split the current libcoq-elpi in a libcoq-elpi
for the purely coq part and a libcoq-elpi-ocaml packages for the
.cma/.cmxs pair?

The binary libcoq-mathcomp-* packages (coming from src:ssreflect, src:mathcomp-bigenouh and src:mathcomp-finmap) have .v, .vo and .glob
files, so there is some coherence.

The src:aac-tactics package builds libaac-tactics-coq with .v, .vo and
.glob files and the documentation, libaac-tactics-ocaml with a
.cmo/.cmxs pair in /usr/lib/ocaml/coq and libaac-tactics-ocaml-dev
provides .cmi and .mli files in /usr/lib/ocaml/coq and documentation (I
think it's code documentation, so puting it in -dev makes sense). libaac-tactics-coq and libaac-tactics-ocaml-dev depend on libaac-
tactic-ocaml, and libaac-tactics-coq recommends libaac-tactics-ocaml.

(3) I'm not sure the current source packages all give good binary
packages (here: names).

You'll have noticed above that the packages I made (either because I
started packaging them or I came along and split an existing one) have
a name starting with libcoq-foo. The various upstreams provide opam
packages, and the names are coq-foo, so I just followed upstream pretty
blindly here, and added a lib prefix because... well, that looked like
libs in some sense.

What I hadn't noticed was src:aac-tactics, where the coq part follows
the libfoo-coq convention. And well, if I look in my /usr/share/doc,
there's libcommons-logging-java, libsereal-decoder-perl, libsexplib-
ocaml... so it's pretty common to use libfoo-<lang> for package names.
But some quick "apt-cache search librust", "apt-cache search libghc", "apt-cache search libjulia" shows other languages follow a prefix
convention. And with golang and erlang, they use <lang>-foo without any
lib prefix!

So basically, if upstream is named foo, the possible conventions could
be:
(1) libfoo-coq, libfoo-ocaml and libfoo-ocaml-dev
(2) libcoq-foo, libcoq-foo-ocaml and libcoq-foo-ocaml-dev
(3) coq-foo, libcoq-foo-ocaml and libcoq-foo-ocaml-dev
(4) coq-foo, libfoo-coq-ocaml and libfoo-coq-ocaml-dev
(5) coq-foo, libfoo-ocaml and libfoo-ocaml-dev

Notice that src:elpi and src:coq-elpi both exist ; the first is a
normal OCaml library and the second, mentioned above, is coq-based, so
the fifth proposition is probably out.

If you want to see more package names in the ecosystem, I have a
comparison page (output of a script I wrote) with the "Coq Platform"
which should help:
https://people.debian.org/~jpuydt/coq_platform.html

Question: Which convention should I follow?

Cheers,

J.Puydt

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

Le 24/03/2022 à 21:59, julien.puydt@gmail.com a écrit :

Question: how are such things done? (pointers to code and/or
documentation are welcome)

I am not aware of a consolidated documentation for that :-( I will try
to share my knowledge on the subject. Feel free to create and/or edit a
page on the wiki :-)


For OCaml packages, a permanent tracker has been set up:

https://release.debian.org/transitions/html/ocaml.html

This is generated by "ben tracker", with configuration from:

https://salsa.debian.org/release-team/transition-data

When an upload breaks packages because they are reverse-dependencies
that must be rebuilt, they appear in red or orange (the tooltip in each
cell indicates the reason). I (manually) schedule binNMUs for these
packages.


There is also a script by nomeata which outputs the following:

https://people.debian.org/~nomeata/binNMUs-ocaml.txt

Some people directly feeds this output to wb. I usually prefer to call
wb myself because nomeata's script only considers release architectures,
and usually when a rebuild is needed, it is needed on all architectures.


To debug testing migrations, you can have a look at the raw output of
the testing migration script:

https://release.debian.org/britney/update_output.txt


There is also the possibility to simulate some testing migration
scenarios with ben, which I find easier for debugging, with the
following commands:

cd /tmp/empty/directory
source /usr/share/doc/ben/examples/migrate/functions.sh
# Downloads package lists for testing/unstable
update
# Simulates a <scenario>
migrate <scenario>
# Shows packages newly broken in testing after simulation
debcheck

<scenario> is a space-separated list of packages that you want to get /
be updated in testing (maybe prefixed by a "_" if you want to have them
removed from testing instead). When "debcheck" returns no error, your <scenario> will eventually execute by itself if it contains no removal
(a hint by the release team might be needed if a removal is actually
needed).

Question: shouldn't I split the current libcoq-elpi in a libcoq-elpi
for the purely coq part and a libcoq-elpi-ocaml packages for the
.cma/.cmxs pair?

This is what I would have done in the initial packaging. I wouldn't do
it now, but for bad reasons (delays in NEW processing).

So basically, if upstream is named foo, the possible conventions could
be:
(1) libfoo-coq, libfoo-ocaml and libfoo-ocaml-dev
(2) libcoq-foo, libcoq-foo-ocaml and libcoq-foo-ocaml-dev
(3) coq-foo, libcoq-foo-ocaml and libcoq-foo-ocaml-dev
(4) coq-foo, libfoo-coq-ocaml and libfoo-coq-ocaml-dev
(5) coq-foo, libfoo-ocaml and libfoo-ocaml-dev
[...]
Question: Which convention should I follow?

I started with libfoo-coq (as I did the aac-tactics initial packaging)
to mimic the ocaml convention... but it is true that no explicit
convention exists. Now that there are more packages with the libcoq-foo convention, I would suggest to stick with that.


Cheers,

--
Stéphane

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

Le lundi 28 mars 2022 à 08:14 +0200, Stéphane Glondu a écrit :

Le 24/03/2022 à 21:59, julien.puydt@gmail.com a écrit :

Question: shouldn't I split the current libcoq-elpi in a libcoq-
elpi
for the purely coq part and a libcoq-elpi-ocaml packages for the
.cma/.cmxs pair?

This is what I would have done in the initial packaging. I wouldn't
do it now, but for bad reasons (delays in NEW processing).

Does the fact that the .cma/.cmxs pair is in /usr/lib/ocaml/coq/user- contrib/elpi/ count?

(I'm still not doing anything, just poking around trying to understand
how things should stand)

Cheers,

J.Puydt

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

Hi,

Le lundi 28 mars 2022 à 08:14 +0200, Stéphane Glondu a écrit :

Le 24/03/2022 à 21:59, julien.puydt@gmail.com a écrit :

Question: how are such things done? (pointers to code and/or
documentation are welcome)

I am not aware of a consolidated documentation for that :-( I will
try to share my knowledge on the subject. Feel free to create and/or
edit a page on the wiki :-)

Uh... that's not team-specific. I tried to read the source code for
dh_ocaml, but things aren't clear (I don't know Perl, that doesn't
help). Things with ocaml:Depends and ocaml:Provides seem to happen at
the end of the file ; I would need to do something like this with
coq:Depends and coq:Provides... or do I?

For OCaml packages, a permanent tracker has been set up:

  https://release.debian.org/transitions/html/ocaml.html

Eh, coq-float provides a libfloat-coq.

This is generated by "ben tracker", with configuration from:

  https://salsa.debian.org/release-team/transition-data

When an upload breaks packages because they are reverse-dependencies
that must be rebuilt, they appear in red or orange (the tooltip in
each cell indicates the reason). I (manually) schedule binNMUs for
these packages.

The "(manually)" is annoying.

There is also a script by nomeata which outputs the following:

  https://people.debian.org/~nomeata/binNMUs-ocaml.txt

Some people directly feeds this output to wb. I usually prefer to
call wb myself because nomeata's script only considers release
architectures, and usually when a rebuild is needed, it is needed on
all architectures.

To debug testing migrations, you can have a look at the raw output of
the testing migration script:

  https://release.debian.org/britney/update_output.txt

There is also the possibility to simulate some testing migration
scenarios with ben, which I find easier for debugging, with the
following commands:

  cd /tmp/empty/directory
  source /usr/share/doc/ben/examples/migrate/functions.sh
  # Downloads package lists for testing/unstable
  update
  # Simulates a <scenario>
  migrate <scenario>
  # Shows packages newly broken in testing after simulation
  debcheck

<scenario> is a space-separated list of packages that you want to get
/
be updated in testing (maybe prefixed by a "_" if you want to have
them
removed from testing instead). When "debcheck" returns no error, your <scenario> will eventually execute by itself if it contains no
removal
(a hint by the release team might be needed if a removal is actually
needed).

Oh, nice.

Question: shouldn't I split the current libcoq-elpi in a libcoq-
elpi
for the purely coq part and a libcoq-elpi-ocaml packages for the
.cma/.cmxs pair?

This is what I would have done in the initial packaging. I wouldn't
do it now, but for bad reasons (delays in NEW processing).

I will still do it: NEW processing is a one-time cost.

So basically, if upstream is named foo, the possible conventions
could be:
(1) libfoo-coq, libfoo-ocaml and libfoo-ocaml-dev
(2) libcoq-foo, libcoq-foo-ocaml and libcoq-foo-ocaml-dev
(3) coq-foo, libcoq-foo-ocaml and libcoq-foo-ocaml-dev
(4) coq-foo, libfoo-coq-ocaml and libfoo-coq-ocaml-dev
(5) coq-foo, libfoo-ocaml and libfoo-ocaml-dev
[...]
Question: Which convention should I follow?

I started with libfoo-coq (as I did the aac-tactics initial
packaging) to mimic the ocaml convention... but it is true that no
explicit convention exists. Now that there are more packages with the libcoq-foo convention, I would suggest to stick with that.

I'm wondering if coq-foo for the foo coq library wouldn't be better:

(1) After all, the package named libcoq-ocaml really is an ocaml
library for 'coq', not an 'ocaml' coq library...

(2) When there's a dh_ocaml AND a dh_coq, having clearly discernable
names might be important. Though perhaps libcoq-ocaml using
ocaml:Depends and not coq:Depends might be enough to avoid collisions.

I would feel better if I knew/understood better how the dh_* files
work... there I know there's a decision to be made but I'm clearly
clueless.

Cheers,

J.Puydt

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

Hello,

On Tue, Mar 29, 2022 at 09:52:16AM +0200, julien.puydt@gmail.com wrote:

Le lundi 28 mars 2022 à 08:14 +0200, Stéphane Glondu a écrit :

Question: shouldn't I split the current libcoq-elpi in a libcoq-
elpi
for the purely coq part and a libcoq-elpi-ocaml packages for the .cma/.cmxs pair?

This is what I would have done in the initial packaging. I wouldn't
do it now, but for bad reasons (delays in NEW processing).

I will still do it: NEW processing is a one-time cost.

You can use the experimental suite for that: just upload splitted
packages to experimental and continue maintaining on the sid branch,
and when the experimental packages have been accepted by ftpmaster
you can carry the split over to sid. I think you have to be careful
with version numbers, though.

-Ralf.

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

Hi,

Le mardi 29 mars 2022 à 23:23 +0200, Ralf Treinen a écrit :

Hello,

On Tue, Mar 29, 2022 at 09:52:16AM +0200,
julien.puydt@gmail.com wrote:

Le lundi 28 mars 2022 à 08:14 +0200, Stéphane Glondu a écrit :

Question: shouldn't I split the current libcoq-elpi in a
libcoq-
elpi
for the purely coq part and a libcoq-elpi-ocaml packages for
the
.cma/.cmxs pair?

This is what I would have done in the initial packaging. I
wouldn't
do it now, but for bad reasons (delays in NEW processing).

I will still do it: NEW processing is a one-time cost.

You can use the experimental suite for that: just upload splitted
packages to experimental and continue maintaining on the sid branch,
and when the experimental packages have been accepted by ftpmaster
you can carry the split over to sid. I think you have to be careful
with version numbers, though.

In the meantime I pushed some things forward :

(1) libcoq-elpi cleared NEW pretty fast with the new binary split ;

(2) I uploaded src:aac-tactics which renames libaac-tactics-cqo to libcoq-aac-tactics to NEW yesterday ;

(3) I think src:coq-float should be removed from Debian, as it seems
abandoned upstream and isn't even part of the Coq Platform.

I'm still digging into dh_ocaml and trying to understand how to adapt
it to coq. I'm clueless what corresponds to md5sums for coq packages ;
even computing deps doesn't look easy.

Should I post a RM: bug on coq-float?

J.Puydt

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