bedrock2
bedrock2 copied to clipboard
mit-plv
how to avoid breakage with coq master?
For obvious reasons, coq devs don't like it when bedrock2 does not build on coq master (even if it builds on latest release) (from https://github.com/mit-plv/bedrock2/issues/120#issuecomment-567499145). We should probably do something about that. Here are my ideas
-
note that breakage on coq master is due to changes in coq, so no matter what we do, it can happen: we pull coq, coq CI pulls bedrock2, coq builds and merges, we build and merge. But hopefully we could get the issues down to just that case.
-
develop using coq master. This would be my favorite, except
- we would need to rebuild it regularly, and preferrably not in a way that blocks us from making progress during that time.
- both coqtail and proofgeneral have been broken with coq master at some time since 8.9
- would we drop support with latest release? if not, we would have the same problem for latest release
-
use an existing web-based CI system, and github pull requests or something. I think the user experience here would slow us down a lot, both for fundamental reasons and for the involvement of web forms.
-
use a chromium-style commit queue and branches that it automatically tries to merge. Is there a service/software that does this?
Note that we ask to test only commits to branches that we track (obviously). So if you work with a typical git workflow on topic branches, you don't have to test your pushes to these branches. Only the merge of these branches to master should be tested before being pushed.
- perhaps coq should test a non-master branch, which would lag master exactly based on what our CI has managed to build on latest coq
https://github.com/mit-plv/bedrock2/issues/120#issuecomment-567509912 I continue to be impressed with your ability to predict coq breakage, I don't think this is a feasible strategy for us (other than devolving to (3)).
Another option: have a branch called ci that you regularly merge master into. You can set up Travis (probably also other CI) to do this automatically, for example, by setting up tokens so that whenever the build on master is successful, you merge the successful commit into ci and then push.
Note that if you follow the route of having a separate branch (maybe stable is a better name than ci?), the opam package should be updated to target it too
- have coq CI test a completely fixed version of this repo, bumped every once in a while. This way we could batch the catch-up work of making things work on coq master. I guess this is essentially the same as 4, except for what to do when coqci branch falls behind master. I used to be a strong proponent for having our code work with latest distributed coq and latest developed coq, but after having put an honestly riddiculous amount of work into this over the last couple of years, I am not sure anymore...
How about this: Let's create a dev branch, on which we do the same "three authors just push whatever they tested locally with one Coq version" as we currently do on master, and install some hook which fast-forwards master to dev whenever CI succeeds on dev.
For now, I pushed my most recent changes to a branch called dev, and I enabled Travis on that branch.
If the build succeeds there, we can fast-forward master to it, and I think I could also write a Github Action which does so automatically.
I am on board with the auto-forward solution.
I would prefer to have the workflow where we to push to master and the autoforward happens on another branch, though (but still email if it fails). In particular, I think it is less bad for to get a not-coq-master-compatible checkout than a stale checkout, and presumably we will be checking out master (and it will be the default branch on github, and so on). I totally admit to having some not-so-clear preference for having master be human-maintained beyond that as well.
I was hesitating about the naming of these two branches and first picked branch-where-we-all-push-to = dev, branch-we-decleare-ready-for-Coq-CI = master, but if you prefer, we can also say branch-where-we-all-push-to = master, branch-we-decleare-ready-for-Coq-CI = tested (or some other name?). I'll keep fiddling with Github's workflows for the autoforward, please ignore failures of that task for the moment.
have coq CI test a completely fixed version of this repo, bumped every once in a while
That is an option that we can explore not just for bedrock2 but for all projects in CI (see coq/coq#6724) but it will take time to get there. Once this is implemented, this should solve problem "0" in the OP.
Regarding dev vs master, just be aware that if master is kept as the default branch, external contributors will very likely base their pull request on master if they don't pay enough attention...
My current plan is to keep using master the way we use it, and to have a special branch called tested whose tip is supposed to always work with Coq master. I wrote this workflow which is supposed to fast-forward tested to master daily at 2am Boston time, if the Travis build on master succeeded.
We'll see tomorrow morning if it worked :wink:
Once everything looks good, I'll submit a PR to the Coq repo so that Coq CI builds tested instead of master.