-
Notifications
You must be signed in to change notification settings - Fork 134
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
CI workflow with current agda master #1051
Comments
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. |
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. |
I'll just talk to the agda maintainers what they think about it. |
The idea is that agda tracks our master, but it is currently moved forward manually. 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). |
The agda CI actually checks cubical (at least a reasonably current version) -> closing. |
Originally posted by @jpoiret in #1014 (comment)
The text was updated successfully, but these errors were encountered: