please update `tested` branch
SkySkimmer opened this issue · 4 comments
It's breaking the bedrock2 dev package (because coqutil.dev gets source from coqutil tested branch)
alternatively you can change the dev package to use master
Oops, sorry for breaking Coq CI (or was it "only" the bench?)
The problem is that the tested branch of coqutil only gets updated to master when someone finds the time and motivation to deal with incompatibilities between 7 different Coq versions, which doesn't happen too frequently... But I guess the dev package only has to work with Coq master? So we could just have it use coqutil's master instead of coqutil's tested branch, as you suggested. But does fiat-crypto depend on the same coqutil dev package in way that would break something there, @JasonGross ?
Yes, the reason I made the dev package depend on tested is so that Fiat Crypto could have a working opam package across all the versions we test
Aah I see...
So we also have a tested branch in bedrock2, which (by CI) is guaranteed to work with Coq master & one recently released Coq version if you use the dependencies as specified by the git submodules in the bedrock2 repo. So the most reliable solution would be to use coqutil at exactly the commit hash given by the coqutil submodule in the bedrock2 repo. Would that be possible?
So the most reliable solution would be to use coqutil at exactly the commit hash given by the coqutil submodule in the bedrock2 repo. Would that be possible?
I'm not sure what you're suggesting here. The coq-coqutil.dev package says that the URL used is git+https://github.com/mit-plv/coqutil.git#tested I don't think there's a URL that corresponds t other latest version of the bedrock2 submodule? The coq-bedrock2.dev package uses the master branch of bedrock2, though...
Maybe it should track tested instead, and the auto-forwarder should refuse to forward if the tracked version of coqutil is not already on coqutil tested?