search

mit-plv / coqutil

Coq library for tactics, basic definitions, sets, maps
MIT License
42 stars 24 forks source link

please update `tested` branch #57

Closed SkySkimmer closed 2 years ago

SkySkimmer commented 2 years ago

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

samuelgruetter commented 2 years ago

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 ?

JasonGross commented 2 years ago

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

samuelgruetter commented 2 years ago

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?

JasonGross commented 2 years ago

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?