Re: On the coq ecosystem in Debian
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
Reply to: