search

mit-plv / bedrock2

A work-in-progress language and compiler for verified low-level programming
http://adam.chlipala.net/papers/LightbulbPLDI21/
MIT License
297 stars 45 forks source link

Bump deps/coqutil from `8b84b7a` to `905ec3c` #378

Closed dependabot[bot] closed 1 year ago

dependabot[bot] commented 1 year ago

Bumps deps/coqutil from 8b84b7a to 905ec3c.

Commits
  • 905ec3c make sure pattern_tuple patterns its arguments right-to-left
  • See full diff in compare view


Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting @dependabot rebase.

Dependabot commands and options
You can trigger Dependabot actions by commenting on this PR: - `@dependabot rebase` will rebase this PR - `@dependabot recreate` will recreate this PR, overwriting any edits that have been made to it - `@dependabot merge` will merge this PR after your CI passes on it - `@dependabot squash and merge` will squash and merge this PR after your CI passes on it - `@dependabot cancel merge` will cancel a previously requested merge and block automerging - `@dependabot reopen` will reopen this PR if it is closed - `@dependabot close` will close this PR and stop Dependabot recreating it. You can achieve the same result by closing it manually - `@dependabot show ignore conditions` will show all of the ignore conditions of the specified dependency - `@dependabot ignore this major version` will close this PR and stop Dependabot creating any more for this major version (unless you reopen the PR or upgrade to it yourself) - `@dependabot ignore this minor version` will close this PR and stop Dependabot creating any more for this minor version (unless you reopen the PR or upgrade to it yourself) - `@dependabot ignore this dependency` will close this PR and stop Dependabot creating any more for this dependency (unless you reopen the PR or upgrade to it yourself)
JasonGross commented 1 year ago

Can this incompatibility be fixed so that bedrock2 works on Coq's bench again? Cf. https://github.com/coq/coq/pull/18145#issuecomment-1757887726

JasonGross commented 1 year ago

CC @andres-erbsen @samuelgruetter

samuelgruetter commented 1 year ago

This dependabot PR is outdated, and bedrock2 already contains the latest coqutil.

dependabot[bot] commented 1 year ago

OK, I won't notify you again about this release, but will get in touch when a new version is available. You can also ignore all major, minor, or patch releases for a dependency by adding an ignore condition with the desired update_types to your config file.

If you change your mind, just re-open this PR and I'll resolve any conflicts on it.

samuelgruetter commented 1 year ago

Can this incompatibility be fixed so that bedrock2 works on Coq's bench again? Cf. coq/coq#18145 (comment)

At some point, I had already pushed a commit to coqutil for which I had not yet updated bedrock2. But at any point in time recently, the submodule commit hash for coqutil in the deps folder of bedrock2 was compatible with bedrock2. Could it be that the bench always takes the latest commit on tested of coqutil, instead of the one that's referenced in the deps folder of bedrock2?

JasonGross commented 1 year ago

Could it be that the bench always takes the latest commit on tested of coqutil, instead of the one that's referenced in the deps folder of bedrock2?

Yes, this is how the opam packages are set up

samuelgruetter commented 1 year ago

Aah ok, so maybe it would be better if a commit in bedrock2's master only makes it onto tested if its coqutil submodule commit hash points to the latest commit of coqutil's tested? Maybe a few more git commands in update-tested.yml would do?

JasonGross commented 1 year ago

Yes, that sounds great! We'll also need to change https://github.com/coq/opam/blob/392081dc02f014e290e7dfbdcf7f1e8a328fd659/extra-dev/packages/coq-bedrock2/coq-bedrock2.dev/opam#L37 to track the tested branch.