Bug#1016416: Coq-related packages transition - coq-elpi

[julien.puydt@gmail.com]

Le dimanche 07 août 2022 à 21:15 +0200, Sebastian Ramacher a écrit :
> On 2022-08-07 11:01:30 +0200, julien.puydt@gmail.com wrote:
> > Hi,
> > 
> > Le mardi 02 août 2022 à 21:43 +0200, Sebastian Ramacher a écrit :
> > > On 2022-07-31 13:23:38 +0200, julien.puydt@gmail.com wrote:
> > > > Package: release.debian.org
> > > > 
> > > > Some Coq-related packages need a rebuild:
> > > > 
> > > > coq-hierarchy-builder
> > > > mathcomp-algebra-tactics mathcomp-analysis
> > > > 
> > > > where packages on the same line can be handled in parallel.
> > > > 
> > > > I can't give a nice ben script because the abi checksum varies
> > > > with
> > > > the
> > > > architecture (see today's mail on debian-devel where I'm trying
> > > > to
> > > > find
> > > > ideas for a better approach).
> > > 
> > > From the discussion on -devel, a permanent tracker like the one
> > > for
> > > Haskell
> > > (https://release.debian.org/transitions/html/haskell.html)
> > > could
> > > help with the rebuilds for coq-* and related packages. Do all
> > > affected
> > > packages depends on some package that we can use as a basis for
> > > the
> > > permapermanent tracker?
> > 
> > Short answer: no.
> 
> What about build-dependencies on dh-coq? Is
> https://release.debian.org/transitions/html/coq.html missing any
> coq-related packages?
> 

The idea to use dh-coq as a marker for Coq-related packages is indeed a
good one, and means no list needs to get updated. Your list does
contain everything in Debian. [Notice: I also have two packages more,
coq-libhyps and coq-relation-algebra -- I have them locally but didn't
upload yet because of pending licensing issues.]

Here is what my script testing installed packages prints ; it should
give an idea of what a full tracker should consider:

Hauteur 1
        coq... ok
Hauteur 2
        aac-tactics... ok
        coq-bignums... ok
        coq-dpdgraph... ok
        coq-elpi... ok
        coq-ext-lib... ok
        coq-hammer... ok
        coq-hott... ok
        coq-libhyps... ok
        coq-menhirlib... ok
        coq-record-update... ok
        coq-reduction-effects... ok
        coq-stdpp... ok
        coq-unicoq... ok
        coq-unimath... ok
        flocq... ok
        ott... ok
        paramcoq... ok
        ssreflect... ok
Hauteur 3
        coq-deriving... ok
        coq-equations... ok
        coq-gappa... ok
        coq-hierarchy-builder... ok
        coq-iris... ok
        coq-math-classes... ok
        coq-mtac2... ok
        coqprime... ok
        coq-reglang... ok
        coq-relation-algebra... ok
        coq-simple-io... ok
        coquelicot... ok
        mathcomp-bigenough... ok
        mathcomp-finmap... ok
        mathcomp-zify... ok
Hauteur 4
        coq-corn... ok
        coq-extructures... ok
        coq-interval... ok
        coq-quickchick... ok
        mathcomp-algebra-tactics... ok
        mathcomp-analysis... ok
        mathcomp-multinomials... ok
        mathcomp-real-closed... ok
Hauteur 5
        coqeal... ok


So checking for dh-coq should give a whole-tree tracker, but does that
help with partial updates?

Cheers,

J.Puydt