Ali Caglayan (Jul 15 2021 at 11:56): Ali Caglayan (Jul 15 2021 at 11:56):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?
Ali Caglayan (Jul 15 2021 at 11:58):https://github.com/tchajed/coq-record-update/pull/23
Ali Caglayan (Jul 15 2021 at 11:59):Are there any plans to update the bedrock2 submodule?
Gaëtan Gilbert (Jul 15 2021 at 12:00):https://github.com/mit-plv/bedrock2/pull/190
Ali Caglayan (Jul 15 2021 at 12:01):The PR seems to still be broken
Théo Zimmermann (Jul 15 2021 at 12:25):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.
Ali Caglayan (Jul 15 2021 at 12:27):Wouldn't it make more sense to move bedrock2 one stage up and depend on its submodules being successfully built in the stage below?
Gaëtan Gilbert (Jul 15 2021 at 12:28):That would be nice, it just needs someone to do it
Ali Caglayan (Jul 15 2021 at 12:31):I'll have a go
Andrej Dudenhefner (Jul 15 2021 at 14:30):coq-record-update looking better now.
Ali Caglayan (Jul 15 2021 at 17:30):I've added the dependencies for bedrock2 and shuffled the stages: https://github.com/coq/coq/pull/14663
Andrej Dudenhefner (Jul 16 2021 at 05:40):Possibly, the coq-record-update bump in bedrock2 went for the master, but not for the tested branch, which is used in ci.
Ali Caglayan (Jul 19 2021 at 11:01):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.
Ali Caglayan (Jul 19 2021 at 11:01):But I will keep the other ci additions, since it is still better than not having them
Last updated: Oct 12 2024 at 13:01 UTC