search

maxsnew / cubical-categorical-logic

Extensions to the cubical stdlib category theory for categorical logic/type theory
MIT License
25 stars 5 forks source link

Peg CI to specific commits #84

Closed maxsnew closed 6 months ago

maxsnew commented 6 months ago

Right now the CI uses the current cubical HEAD, which leads to CI breaking unpredictably based on when there is a breaking change upstream. This has happened twice in the last week. IMO these are "false negatives" where there isn't really anything broken in our code. Instead we should peg the CI to use a particular tag/commit from cubical and then we manually update the CI when we want to sync up with the upstream cubical library.

Thoughts? @hejohns @stschaef

hejohns commented 6 months ago

Contingent on others' feedback, I prefer having the CI build against cubical/master. I'd like to keep the time window where we have incompatibilities with cubical/master as small as possible. I'm afraid of writing even more code ignorant of the upstream changes, that then requires additional work to fix. And I don't find the downsides to our current approach too severe.

If we want to explicitly track the upstream version we're compatible with, is there anything wrong with an in-repo git submodule for cubical?

maxsnew commented 6 months ago

The downside is that CI is broken randomly by things out of control of this repo. So e.g., CI doesn't work on pull requests right now even though there's nothing wrong with the PRs. There's no reason we should have to block reviewing internal PRs because a breaking change was made upstream. Maybe we can have some separate CI that gives us a warning if there's a breaking change upstream, but I don't want a red X that's outside of our control.

is there anything wrong with an in-repo git submodule for cubical?

I'd prefer to use Agda's normal agda-lib stuff rather than hacking our own package management.

hejohns commented 6 months ago

Oh I see now that the breakage is because https://github.com/agda/cubical/pull/1108 w/ @maxsnew and @stschaef got merged.

How is this usually handled? Eg I could remove every duplicate symbol from cubical-categorical-logic, but I'd probably miss functions that were renamed for the upstream PR but kept here?

maxsnew commented 6 months ago

Steven or I will take care of it since we're familiar with what was changed. We just remove things here that are upstream now, and add .More files as necessary if modules have been added upstream.