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.
That is presumably a consequence of https://github.com/coq/coq/pull/13958 . Did you rebase your branch on top of master?
MetaCoq is still missing the overlay for sordid reasons, it seems
Ah, no, sorry, confusing with what happened with Mtac
Rebasing is not required these days. Coqbot performs an automatic merge with master.
But it's still missing the overlay
I will harass somebody on the gallinette mattermost to see if we get a quick answer
I just rebased, let's see how it goes.
it will fail as well
Why? master
contains the overlay, does it not?
the overlay would only trigger on that PR
Oh! I didn't know overlays were not permanent. Isn't that bound to cause a lot of pain?
We've been living like that for quite a time already, so it's not that horrible
I thought the protocol for merging a PR which needs overlays was to first update the deps and then merge the PR.
The overlay has been merged.
@Anton Trunov that would break Coq as well
Indeed, didn't think about that.
This is the protocol for backward-compatible overlays.
For backward-incompatible ones, the protocol is to try to merge everything at once.
But it always create sync issues (fortunately not that many and not that frequently).
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
It's working now. Thanks everyone!
Last updated: May 31 2023 at 16:01 UTC