Stream: math-comp analysis

Topic: CI?


view this post on Zulip Bas Spitters (Nov 17 2021 at 14:30):

Analysis seems to be missing here. Would it be interesting to add it?
https://github.com/coq/coq/tree/master/dev/ci
We are depending on it for SSProve.

view this post on Zulip Reynald Affeldt (Nov 17 2021 at 14:40):

Thanks for the pointer (and for using mathcomp-analysis). This will be on the agenda of the next meeting if we can't do it before.

view this post on Zulip Enrico Tassi (Nov 17 2021 at 16:46):

FTR it is in the coq platform CI, which does not run at each commit in coq, but rather once a day.

view this post on Zulip Karl Palmskog (Nov 17 2021 at 16:46):

also in the MathComp CI, right? We are getting a lot of CIs left and right...

view this post on Zulip Enrico Tassi (Nov 17 2021 at 16:46):

yes

view this post on Zulip Karl Palmskog (Nov 17 2021 at 16:48):

I think that we should establish a policy on CI redundancy. For plugins, they have to be in Coq's CI to be in the platform, but regular Coq projects that are in Platform CI and MathComp CI don't have to be, and shouldn't be - at least this is my view

view this post on Zulip Karl Palmskog (Nov 17 2021 at 16:49):

I would go so far as claiming that MathComp projects seldom break because of Coq itself, but mostly because of MathComp changes...

view this post on Zulip Enrico Tassi (Nov 17 2021 at 16:53):

This is true, but sometime CI tests different things. Eg the platform makes packages, which may also break if make install becomes bogus. MC ci uses nix, not opam, so it may not catch all the same errors. But I agree the overlap is probably too much

view this post on Zulip Bas Spitters (Nov 18 2021 at 13:30):

@Enrico Tassi @Karl Palmskog Thanks. Sometimes it's a bit hard to get an overview of what's where...


Last updated: Aug 19 2022 at 19:03 UTC