Julien Puydt (Feb 07 2022 at 11:57): Julien Puydt (Feb 07 2022 at 11:57):Hi, I will want to work on packaging mc-analysis for Debian ; I don't think we have all the deps right at the moment.
Are they fixed or will some of them be merged (in mc or mc-analysis) in the very near future?
Karl Palmskog (Feb 07 2022 at 12:00):I think you will have to define what you mean by "all the deps right". For example, 0.3.13 shipped recently in the Coq Platform: https://github.com/coq/platform/blob/main/doc/README~8.15~beta1.md
... so it had no obvious dependency problems.
Karl Palmskog (Feb 07 2022 at 12:02):if you want to package Coq ecosystem libraries, we strongly advise following the Platform picks, otherwise there are no hard guarantees that one package will be compatible with another. We do test continuously in the opam archive, but we can't account for all possible combinations of Coq/MathComp/plugins
Julien Puydt (Feb 07 2022 at 12:22):Ah, I meant that it depends on mc which Debian has, but also on MC-finmap and MC-bigenough which isn't there yet.
There's little point in packaging one of those if they get merged (in MC or MC-analysis) on a short timescale, so that's the goal of my question.
Cyril Cohen (Feb 07 2022 at 12:42):These is no merge of finmap or bigenough scheduled in the short-term, only on the middle-term (but it's been the case for a while)
Karl Palmskog (Feb 07 2022 at 12:44):and here I thought the packaging challenge was Hierarchy Builder (+Coq-Elpi)
Julien Puydt (Feb 07 2022 at 15:25):Well, I knew that was the big morsel, so I worked on it first: https://tracker.debian.org/pkg/coq-hierarchy-builder (and https://tracker.debian.org/pkg/coq-elpi).
Enrico Tassi (Feb 07 2022 at 18:15):Would you mind upstreaming the patches to Coq-Elpi (some typos got in already, but you seem to have more)
Enrico Tassi (Feb 07 2022 at 18:16):(I'm planning an release very very soon, even tomorrow it possible)
Julien Puydt (Feb 07 2022 at 21:11):@Enrico Tassi I have two patches, and according to the comments there, I already forwarded them: https://github.com/LPCIC/coq-elpi/issues/306 and https://github.com/LPCIC/coq-elpi/issues/307
Enrico Tassi (Feb 07 2022 at 21:15):Ah ok, the issue contains a patch. I'll apply it.
Julien Puydt (Feb 09 2022 at 14:02):Ok, I have now packaged finmap, bigenough and analysis for Debian -- they're in the NEW queue, waiting for a manual review of the copyrights. They could be there for months, but they'll get in eventually! https://ftp-master.debian.org/new.html -- search for mathcomp
Last updated: Oct 13 2024 at 01:02 UTC