Anton Trunov (Mar 31 2021 at 07:40): 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.
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?
Pierre-Marie Pédrot (Mar 31 2021 at 07:50):MetaCoq is still missing the overlay for sordid reasons, it seems
Pierre-Marie Pédrot (Mar 31 2021 at 07:51):Ah, no, sorry, confusing with what happened with Mtac
Théo Zimmermann (Mar 31 2021 at 07:51):Rebasing is not required these days. Coqbot performs an automatic merge with master.
Pierre-Marie Pédrot (Mar 31 2021 at 07:51):But it's still missing the overlay
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
Anton Trunov (Mar 31 2021 at 07:53):I just rebased, let's see how it goes.
Pierre-Marie Pédrot (Mar 31 2021 at 07:54):it will fail as well
Guillaume Melquiond (Mar 31 2021 at 07:55):Why? master contains the overlay, does it not?
Pierre-Marie Pédrot (Mar 31 2021 at 07:56):the overlay would only trigger on that PR
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?
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
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.
Pierre-Marie Pédrot (Mar 31 2021 at 08:06):The overlay has been merged.
Pierre-Marie Pédrot (Mar 31 2021 at 08:06):@Anton Trunov that would break Coq as well
Anton Trunov (Mar 31 2021 at 08:07):Indeed, didn't think about that.
Théo Zimmermann (Mar 31 2021 at 08:11):This is the protocol for backward-compatible overlays.
Théo Zimmermann (Mar 31 2021 at 08:11):For backward-incompatible ones, the protocol is to try to merge everything at once.
Théo Zimmermann (Mar 31 2021 at 08:12):But it always create sync issues (fortunately not that many and not that frequently).
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
Anton Trunov (Mar 31 2021 at 10:11):It's working now. Thanks everyone!
Last updated: Dec 07 2023 at 17:01 UTC