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

Adapt to https://github.com/coq/coq/pull/18880 #415

Closed proux01 closed 6 months ago

proux01 commented 6 months ago

Adapt to https://github.com/coq/coq/pull/18880

We should implement the nice suggestion of @andres-erbsen https://github.com/coq/coq/pull/18880#discussion_r1550304610 to save the Existing Instance but meanwhile, this is probably good enough for now.

proux01 commented 6 months ago

Thanks

proux01 commented 6 months ago

@andres-erbsen Out of curiosity, how/when is that expected to be updated in the fiat-crypto submodule?

JasonGross commented 6 months ago

If https://github.com/mit-plv/rupicola/pull/110 is merged then dependabot will create a PR in rupicola within a day, otherwise a maintainer needs to trigger dependabot manually (I don't have the bits to do this). Once the PR in rupicola is merged, dependabot will create a PR in Fiat Crypto within a day (or you can ping me and I can trigger it sooner), and then I can set that PR to merge once CI passes (generally a couple hours).

Note that with https://github.com/coq/coq/pull/18736, even though this PR is merged, you can set up an overlay bedrock2 https://github.com/mit-plv/bedrock2 master $PR_NUMBER and not have the Coq PR blocked on submodule updates.

proux01 commented 6 months ago

Thanks for the explanation (and indeed, monthly really looks pretty slow, particularly if the is another month in fiat-crypto itself)

Note that with https://github.com/coq/coq/pull/18736, even though this PR is merged, you can set up an overlay bedrock2 https://github.com/mit-plv/bedrock2 master $PR_NUMBER and not have the Coq PR blocked on submodule updates.

I was hoping to save the overlay, but I guess I won't escape it ;-)