• Coq-based packages

    From Julien Puydt@21:1/5 to All on Fri Feb 4 23:40:01 2022
    Hi,

    I just changed the binary packages provided by the source coq package
    to follow more closely upstream's subpackages. I used
    Provides+Breaks+Replaces so things should go smoothly.

    Now I would like to work on other things:

    (1) the source package coq-doc (non-free) should be updated to latest
    upstream, to follow more closely what we provide as coq ;

    (2) the source package ssreflect provides libssreflect-coq ; in fact
    it's packaging what upstream calls mathcomp, and should provide things
    like libcoq-mathcomp-algebra, libcoq-mathcomp-character, libcoq- mathcomp-field, libcoq-mathcomp-fingroup, libcoq-mathcomp-solvable and libcoq-mathcomp-ssreflect (all with Breaks on libssreflect-coq) -- and
    probably a libcoq-mathcomp depending on the previous list (with Breaks+Provides+Replaces on libssreflect-coq).

    (3) the source package mathcomp exists, and doesn't provide anything ;
    in fact it was just imported two years ago in salsa from anonscm, and
    didn't see any activity.

    (4) I'll want to package https://github.com/math-comp/analysis (as src:mathcomp-analysis providing libcoq-mathcomp-analysis)
    [aside: that's the reason why above I propose the name libcoq-mathcomp
    and not libcoq-mathcomp-all...]

    For point (1), I think I can go ahead just now.

    To deal with points (2) and (3), I'll definitely want the new
    src:mathcomp and binary packages to derive from the current
    src:ssreflect package, but for that some actions will have to be made
    by team managers:

    - salsa's mathcomp should be put out of the way (where?) ;

    - salsa's ssreflect should be renamed to mathcomp.

    Point (4) can wait until points (1)-(3) are done.

    Does that plan sound ok?

    Cheers,

    J.Puydt

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