CI workflow with current agda master about cubical

[felixwellen]

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]

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]

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

[felixwellen]

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]

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