Stream: math-comp devs

Topic: Lemma overloading


view this post on Zulip Karl Palmskog (Nov 30 2023 at 13:59):

We have this "tutorial" MathComp repo in Coq-community that hasn't received a lot of updates lately: https://github.com/coq-community/lemma-overloading

Might this repo be welcome in MathComp's CI if we make it build with MathComp dev?

view this post on Zulip Pierre Roux (Nov 30 2023 at 14:24):

Well, if it's unmaintained I'd rather not add it to the CI because it would mean mathcomp devs would have to maintain it.

view this post on Zulip Karl Palmskog (Nov 30 2023 at 15:53):

well, it's "community maintained" at this point. If there are tasks deemed required by mathcomp devs to stay in CI, volunteers like me could pitch in

view this post on Zulip Pierre Roux (Nov 30 2023 at 16:05):

Mathcomp's CI is not that formal, maybe we can try. The first step for addition in CI is creating a Nix package (see e.g. https://github.com/NixOS/nixpkgs/pull/231077 )


Last updated: Jul 23 2024 at 21:01 UTC