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
