Stream: math-comp analysis

Topic: Debian packaging


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Karl Palmskog (Feb 07 2022 at 12:44):

and here I thought the packaging challenge was Hierarchy Builder (+Coq-Elpi)

view this post on Zulip 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).

view this post on Zulip 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)

view this post on Zulip Enrico Tassi (Feb 07 2022 at 18:16):

(I'm planning an release very very soon, even tomorrow it possible)

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Feb 07 2022 at 21:15):

Ah ok, the issue contains a patch. I'll apply it.

view this post on Zulip 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: Aug 19 2022 at 20:03 UTC