search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
446 stars 136 forks source link

CI workflow with current agda master #1051

Closed felixwellen closed 3 months ago

felixwellen commented 11 months ago 
          Setting up CI now would help noticing breaking changes faster instead of having to look at a whole release's changelog. It will eat up more CI time the way it is currently set up though as the job will also rebuild Agda itself. I wonder if/how we could re-use the main agda repo's artifacts.

Originally posted by @jpoiret in https://github.com/agda/cubical/issues/1014#issuecomment-1715258184

felixwellen commented 11 months ago

I can see that (in principle) it would be good to know if the library checks with the current agda master. I don't think it would be good to have that as a CI job though, since it would mean we have to hit a moving target. I remember that in the last months there were times when the library checked with agda master and times when it didn't. So I suspect we would be forced to deal with regressions of agda if we put a workflow with agda master in our CI.

jpoiret commented 11 months ago

But for the times when the library doesn't check anymore because eg. something was fixed, it would be nice to know right as the bug is fixed. In the case of regressions, they could also be notified upstream, I'm not sure they have CI checks on cubical anymore (or they use a fixed commit in the past which might be suboptimal).

I don't have a strong opinion either way. You could also consider just adding it but not making it blocking for PRs, just to check on the status with upstream's master periodically.

felixwellen commented 11 months ago

I'll just talk to the agda maintainers what they think about it.

felixwellen commented 11 months ago

The idea is that agda tracks our master, but it is currently moved forward manually. If someone makes a PR that makes the agda CI check against our current master, that should be an improvement. Then, however, we should react if there are breaking changes - but I guess we can do that.

More unrelated, we are the slowest thing in the agda CI at that stage with our ~30min. So it would be good to get that down (see #748).

felixwellen commented 3 months ago

The agda CI actually checks cubical (at least a reasonably current version) -> closing.