There is a persistent CI failure with bedrock2. They seem to be from coq-record-update. Perhaps we should add coq-record-update to the CI?
Are there any plans to update the bedrock2 submodule?
The PR seems to still be broken
Technically, coq-record-update is part of the CI since it is a dependency of bedrock2. However, it is indeed a pain that many projects in CI declare such implicit dependencies using submodules because it makes their management way more complex for us.
Wouldn't it make more sense to move bedrock2 one stage up and depend on its submodules being successfully built in the stage below?
That would be nice, it just needs someone to do it
I'll have a go
coq-record-update looking better now.
I've added the dependencies for bedrock2 and shuffled the stages: https://github.com/coq/coq/pull/14663
Possibly, the coq-record-update bump in bedrock2 went for the
master, but not for the
tested branch, which is used in ci.
I really couldn't get this to work. I think there is an issue with bedrock2's makefile so I submitted an issue. For now, I am thinking of reverting to using submodules in building bedrock2 since I know that works.
But I will keep the other ci additions, since it is still better than not having them
Last updated: Oct 16 2021 at 09:07 UTC