Bas Spitters (Nov 17 2021 at 14:30): 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.
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.
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.
Karl Palmskog (Nov 17 2021 at 16:46):also in the MathComp CI, right? We are getting a lot of CIs left and right...
Enrico Tassi (Nov 17 2021 at 16:46):yes
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
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...
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
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: Apr 19 2024 at 08:01 UTC