Re: On the coq ecosystem in Debian

[Stéphane Glondu <glondu@debian.org>]

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