Beta Ziliani (Sep 23 2020 at 18:58): Beta Ziliani (Sep 23 2020 at 18:58):Hi! The CI of Mtac2 is failing to compile coq.dev from opam. It seems the problem is in the configuration, although I can't see what's wrong. Was there any relevant change lately? Thanks.
Gaëtan Gilbert (Sep 23 2020 at 19:11): Gaëtan Gilbert (Sep 23 2020 at 19:12):do you not run opam update?
Beta Ziliani (Sep 23 2020 at 19:28)::face_palm: sorry for missing that line. I don't understand though, shouldn't it be in the opam description file that it requires 1.10?
Beta Ziliani (Sep 23 2020 at 19:28):I mean, why is opam installing the 1.9?
Enrico Tassi (Sep 23 2020 at 19:46):update fetches an up to date package list (upgrades installs the last known version).
Beta Ziliani (Sep 23 2020 at 19:55):since it's a batch run from a clean machine, that shouldn't be the issue
Enrico Tassi (Sep 23 2020 at 20:01):Hum, I see a docker image. Was it generated recently? because it seems to contain the opam root.
Théo Zimmermann (Sep 23 2020 at 20:03):May I ask why you are using a basic OCaml image instead of Docker-Coq?
Janno (Sep 23 2020 at 20:36):The coq docker imagine is usually out of date by a day or so and we only allow PRs to be merged that pass CI. This poses a problem for overlays that should to be merged quickly after the corresponding Coq PR is merged. To work around this we rebuild Coq/master for every CI run.
Janno (Sep 23 2020 at 20:38):And for that it seemed unnecessary to use the Coq docker image but I guess now we see that the image could still be useful even if we rebuild Coq.
Paolo Giarrusso (Sep 23 2020 at 20:38):IIUC "opam install -y coq.dev" is installing the wrong zarith and then failing
Paolo Giarrusso (Sep 23 2020 at 20:39):So that seems a bug in the package as Beta was suggesting.
Paolo Giarrusso (Sep 23 2020 at 20:40):OTOH, https://travis-ci.org/github/Mtac2/Mtac2/builds/729658147#L441 does not include an opam update, and that seems a bug in the CI script.
Paolo Giarrusso (Sep 23 2020 at 20:41):if the base image it out of date enough, and coq.dev upgraded dependencies, then the CI would fail due to the missing opam update.
Paolo Giarrusso (Sep 23 2020 at 20:42):separately, Opam does not actually guarantee that it’ll pick the latest applicable zarith, IME.
Paolo Giarrusso (Sep 23 2020 at 20:42):I’ve seen opam install coq-stdpp both upgrade num and downgrade num.
Paolo Giarrusso (Sep 23 2020 at 20:43):so either opam uses some SAT solver without scoring solutions, or the scoring is buggy.
Paolo Giarrusso (Sep 23 2020 at 20:45):sent PR for the bug @Beta Ziliani found (untested): https://github.com/coq/opam-coq-archive/pull/1429
Paolo Giarrusso (Sep 23 2020 at 20:45):I just edited the file from a browser
Beta Ziliani (Sep 23 2020 at 20:48):but why would one need to opam update recently added repositories?
Paolo Giarrusso (Sep 23 2020 at 20:48):Not the ones you just added, but the main one.
Paolo Giarrusso (Sep 23 2020 at 20:48):Dunno, but doesn't zarith come from the basic opam repo?
Paolo Giarrusso (Sep 23 2020 at 20:49):If the opam update is done by the image, and the image is updated by somebody else, that could be fine.
Paolo Giarrusso (Sep 23 2020 at 20:50):Looking at the log, the point is in particular to run "opam update default"
Paolo Giarrusso (Sep 23 2020 at 20:53):But if the base image is updated often enough, omitting that might only break in rare cases.
Théo Zimmermann (Sep 23 2020 at 21:00):Janno said:
The coq docker imagine is usually out of date by a day or so and we only allow PRs to be merged that pass CI. This poses a problem for overlays that should to be merged quickly after the corresponding Coq PR is merged. To work around this we rebuild Coq/master for every CI run.
Have you considered using a Nix based CI then? Thanks to Cachix, you can still get a pre-built Coq that is as fresh as can be. This is supported by our Travis template here: https://github.com/coq-community/templates
Théo Zimmermann (Sep 23 2020 at 21:01): Théo Zimmermann (Sep 24 2020 at 07:28):In fact, that wouldn't work for your use case because the OCaml version it uses is too recent for UniCoq + Mtac2 :frown:
Enrico Tassi (Sep 24 2020 at 07:50):@Théo Zimmermann do you have a pointer for the problems about ocaml + unicoq/mtac2 ? (I want to understand if the same can/could apply to Elpi)
Emilio Jesús Gallego Arias (Sep 24 2020 at 12:40):@Enrico Tassi that's the doubly linking bug due to the way coq_makefile links , there are a couple of issues in the bug tracker
Emilio Jesús Gallego Arias (Sep 24 2020 at 12:40):Regarding docker, it would not be too hard to push a docker image with coq master for each commit, as done with cachix, just needs someone to do it [maybe the most challenging bit is GC of images]
Beta Ziliani (Sep 24 2020 at 15:15):After re-compiling Coq I see that I can't compile Unicoq because of a Dynlink error, is this the problem @Théo Zimmermann ?
Enrico Tassi (Sep 24 2020 at 15:22):I think I found the relevant issue, maybe it's better to discuss the dynlink problem there.
Paolo Giarrusso (Sep 24 2020 at 16:07):@Théo Zimmermann the wiki says Nix uses OCaml 4.06.1, is that stale?
Théo Zimmermann (Sep 24 2020 at 17:23):Oh yes, that's stale sorry about that. The real value is here: https://github.com/coq/coq/blob/master/default.nix#L25
Théo Zimmermann (Sep 24 2020 at 17:23):So 4.09.
Théo Zimmermann (Sep 24 2020 at 17:24):Beta Ziliani said:
After re-compiling Coq I see that I can't compile Unicoq because of a Dynlink error, is this the problem Théo Zimmermann ?
Yes, that's the issue.
Théo Zimmermann (Sep 24 2020 at 17:27):Emilio Jesús Gallego Arias said:
Regarding docker, it would not be too hard to push a docker image with coq master for each commit, as done with cachix, just needs someone to do it [maybe the most challenging bit is GC of images]
Well in fact, we could certainly auto-trigger a build on https://gitlab.com/coq-community/docker-coq every time master is updated (this was not done initially because the build used to be on Docker Hub). There is no garbage collection issue because this is always overriding the same tag on Docker Hub (tag dev, see https://hub.docker.com/r/coqorg/coq/tags). cc @Erik Martin-Dorel (seems something worth doing)
Théo Zimmermann (Sep 24 2020 at 17:31): Théo Zimmermann (Sep 24 2020 at 17:32):Since it is coqbot triggering pipelines on our GitLab and it also has access to the coq-community organization, this should work.
Beta Ziliani (Sep 25 2020 at 19:10):OK, I don't understand almost any of all the layers that are in place here, so I'm just stabbing in the air. I'm using now a docker image with OCaml 4.09, and after opam update system it seems to not have zarith 1.10. Any clues? (log here )
Beta Ziliani (Sep 25 2020 at 19:13):(while at it I also don't understand why locally I do have that version of zarith, with the same version of OCaml, and why I can compile Coq with the former version of zarith)
Gaëtan Gilbert (Sep 25 2020 at 19:18):your docker image uses a static local repo for the default repo, so update does nothing
Gaëtan Gilbert (Sep 25 2020 at 19:19):what does configure say for you locally?
Gaëtan Gilbert (Sep 25 2020 at 19:19):and what coq commit?
Beta Ziliani (Sep 25 2020 at 19:36):hehe configure fails :)
ok, that solves the later half. about the former half, I accept suggestions for docker images
Gaëtan Gilbert (Sep 25 2020 at 19:58):just remove the default repo and use the online one instead
Théo Zimmermann (Sep 26 2020 at 11:22):Or just use the base image of Docker-Coq: https://hub.docker.com/r/coqorg/base#supported-tags
Théo Zimmermann (Sep 26 2020 at 11:22):The zarith version is the right one.
Beta Ziliani (Sep 26 2020 at 20:45):I'm taking Théo's advice now, although there is no "base" image, but "bare" and it's too bare, so I'm using "latest". Seems to be working.
Théo Zimmermann (Sep 27 2020 at 09:28):"base" is the name of the image itself, I was not talking about the tag.
Beta Ziliani (Sep 27 2020 at 19:34):Thanks guys. Now we are facing a different issue now (bors being dead).
Last updated: Sep 09 2024 at 04:02 UTC