Analysis seems to be missing here. Would it be interesting to add it?
We are depending on it for SSProve.
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.
FTR it is in the coq platform CI, which does not run at each commit in coq, but rather once a day.
also in the MathComp CI, right? We are getting a lot of CIs left and right...
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
I would go so far as claiming that MathComp projects seldom break because of Coq itself, but mostly because of MathComp changes...
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
@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