Stream: Coq devs & plugin devs

Topic: CI: MetaCoq is failing


view this post on Zulip Anton Trunov (Mar 31 2021 at 07:40):

MetaCoq is failing in CI due to, I believe, an unrelated reason, please see https://gitlab.com/coq/coq/-/jobs/1142202657:

CAMLOPT -c -for-pack Template_coq src/denoter.ml
2120File "src/denoter.ml", line 114, characters 34-62:
2121Error: Unbound module Recordops
2122Command exited with non-zero status 2
2123src/denoter.cmx (real: 0.20, user: 0.02, sys: 0.03, mem: 18720 ko)
2124Makefile.template:668: recipe for target 'src/denoter.cmx' failed

This is the PR I'm talking about: https://github.com/coq/coq/pull/13069.

view this post on Zulip Guillaume Melquiond (Mar 31 2021 at 07:46):

That is presumably a consequence of https://github.com/coq/coq/pull/13958 . Did you rebase your branch on top of master?

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 07:50):

MetaCoq is still missing the overlay for sordid reasons, it seems

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 07:51):

Ah, no, sorry, confusing with what happened with Mtac

view this post on Zulip Théo Zimmermann (Mar 31 2021 at 07:51):

Rebasing is not required these days. Coqbot performs an automatic merge with master.

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 07:51):

But it's still missing the overlay

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 07:52):

I will harass somebody on the gallinette mattermost to see if we get a quick answer

view this post on Zulip Anton Trunov (Mar 31 2021 at 07:53):

I just rebased, let's see how it goes.

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 07:54):

it will fail as well

view this post on Zulip Guillaume Melquiond (Mar 31 2021 at 07:55):

Why? master contains the overlay, does it not?

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 07:56):

the overlay would only trigger on that PR

view this post on Zulip Guillaume Melquiond (Mar 31 2021 at 07:58):

Oh! I didn't know overlays were not permanent. Isn't that bound to cause a lot of pain?

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:04):

We've been living like that for quite a time already, so it's not that horrible

view this post on Zulip Anton Trunov (Mar 31 2021 at 08:06):

I thought the protocol for merging a PR which needs overlays was to first update the deps and then merge the PR.

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:06):

The overlay has been merged.

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:06):

@Anton Trunov that would break Coq as well

view this post on Zulip Anton Trunov (Mar 31 2021 at 08:07):

Indeed, didn't think about that.

view this post on Zulip Théo Zimmermann (Mar 31 2021 at 08:11):

This is the protocol for backward-compatible overlays.

view this post on Zulip Théo Zimmermann (Mar 31 2021 at 08:11):

For backward-incompatible ones, the protocol is to try to merge everything at once.

view this post on Zulip Théo Zimmermann (Mar 31 2021 at 08:12):

But it always create sync issues (fortunately not that many and not that frequently).

view this post on Zulip Théo Zimmermann (Mar 31 2021 at 08:13):

FTR I've proposed in the past to adopt a different model, but the discussion was long and painful: https://github.com/coq/coq/issues/6724

view this post on Zulip Anton Trunov (Mar 31 2021 at 10:11):

It's working now. Thanks everyone!


Last updated: Oct 15 2021 at 19:03 UTC