src/Bedrock/Field/Common/Util.v broken
bMacSwigg opened this issue · 3 comments
Running make coq from my fork's main branch (no local changes, up-to-date with mit-plv/fiat-crypto) fails in compiling src/Bedrock/Field/Common/Util.v:
File "./src/Bedrock/Field/Common/Util.v", line 1038, characters 6-37:
Error: Expected a single focused goal but 3 goals are focused.
Is it possible the submodules are outdated? (Try git submodule update --recursive)
Yep that seems to be the issue. After updating the submodules, make src/Bedrock/Field/Common/Util.vo succeeds. Confirming by re-running make coq now, but it seems likely that this fixes it.
Out of curiosity, how could you tell that was the issue? :)
The CI passes and you're reporting an issue in one of the files that depends on bedrock, and Sam recently merged a PR that bumped the submodules. Since git doesn't automatically update submodules on pull / checkout, this has become one of the first things I think of when something is going wrong with the bedrock files for no apparent reason.