search

mit-plv / kami

A Platform for High-Level Parametric Hardware Specification and its Modular Verification
https://plv.csail.mit.edu/kami/
MIT License
142 stars 24 forks source link

Adapt to coq/coq#13837 ("apply with" does not rename arguments) #27

Closed SkySkimmer closed 3 years ago

SkySkimmer commented 3 years ago

Should be backwards compatible.

SkySkimmer commented 3 years ago

Please merge now and bump the submodule in bedrock2

samuelgruetter commented 3 years ago

I checked out 17c92d4a33468356bb9f9dfa537ca74bab48bd1b locally and built it with ./skip_proof.sh -r && make, to make sure the proofs that are too expensive for CI also are checked. Then I fast-forwarded the rv32i branch to that commit. However, I see that in the mean time, @SkySkimmer made a few force pushes, and @andres-erbsen already merged https://github.com/mit-plv/bedrock2/pull/199, which references 1df3755b86d1f97153d20edf51f2b0b897cf7640, which is the lastest force push as of now.

So we are now in the somewhat inconsistent state that bedrock2 references a commit that is not the tip of kami's rv32i branch, but a commit in @SkySkimmer's fork.

Do you expect that more changes will be needed @SkySkimmer ?

SkySkimmer commented 3 years ago

No more changes expected to bedrock and bedrock deps.

samuelgruetter commented 3 years ago

Ok, so I force-pushed rv32i to 1df3755b86d1f97153d20edf51f2b0b897cf7640, so things should be back in sync again.