Stream: Coq devs & plugin devs

Topic: CI failure with bedrock2


view this post on Zulip 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?

view this post on Zulip Ali Caglayan (Jul 15 2021 at 11:58):

https://github.com/tchajed/coq-record-update/pull/23

view this post on Zulip Ali Caglayan (Jul 15 2021 at 11:59):

Are there any plans to update the bedrock2 submodule?

view this post on Zulip Gaëtan Gilbert (Jul 15 2021 at 12:00):

https://github.com/mit-plv/bedrock2/pull/190

view this post on Zulip Ali Caglayan (Jul 15 2021 at 12:01):

The PR seems to still be broken

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Jul 15 2021 at 12:28):

That would be nice, it just needs someone to do it

view this post on Zulip Ali Caglayan (Jul 15 2021 at 12:31):

I'll have a go

view this post on Zulip Andrej Dudenhefner (Jul 15 2021 at 14:30):

coq-record-update looking better now.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 16 2021 at 09:07 UTC