Stream: Coq devs & plugin devs

Topic: Failing to compile coq.dev


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

view this post on Zulip Gaëtan Gilbert (Sep 23 2020 at 19:11):

Zarith version 1.10 is required, you have 1.9.1

view this post on Zulip Gaëtan Gilbert (Sep 23 2020 at 19:12):

do you not run opam update?

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

view this post on Zulip Beta Ziliani (Sep 23 2020 at 19:28):

I mean, why is opam installing the 1.9?

view this post on Zulip Enrico Tassi (Sep 23 2020 at 19:46):

update fetches an up to date package list (upgrades installs the last known version).

view this post on Zulip Beta Ziliani (Sep 23 2020 at 19:55):

since it's a batch run from a clean machine, that shouldn't be the issue

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

view this post on Zulip Théo Zimmermann (Sep 23 2020 at 20:03):

May I ask why you are using a basic OCaml image instead of Docker-Coq?

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

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

view this post on Zulip Paolo Giarrusso (Sep 23 2020 at 20:38):

IIUC "opam install -y coq.dev" is installing the wrong zarith and then failing

view this post on Zulip Paolo Giarrusso (Sep 23 2020 at 20:39):

So that seems a bug in the package as Beta was suggesting.

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

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

view this post on Zulip Paolo Giarrusso (Sep 23 2020 at 20:42):

separately, Opam does not actually guarantee that it’ll pick the latest applicable zarith, IME.

view this post on Zulip Paolo Giarrusso (Sep 23 2020 at 20:42):

I’ve seen opam install coq-stdpp both upgrade num and downgrade num.

view this post on Zulip Paolo Giarrusso (Sep 23 2020 at 20:43):

so either opam uses some SAT solver without scoring solutions, or the scoring is buggy.

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

view this post on Zulip Paolo Giarrusso (Sep 23 2020 at 20:45):

I just edited the file from a browser

view this post on Zulip Beta Ziliani (Sep 23 2020 at 20:48):

but why would one need to opam update recently added repositories?

view this post on Zulip Paolo Giarrusso (Sep 23 2020 at 20:48):

Not the ones you just added, but the main one.

view this post on Zulip Paolo Giarrusso (Sep 23 2020 at 20:48):

Dunno, but doesn't zarith come from the basic opam repo?

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

view this post on Zulip Paolo Giarrusso (Sep 23 2020 at 20:50):

Looking at the log, the point is in particular to run "opam update default"

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

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

view this post on Zulip Théo Zimmermann (Sep 23 2020 at 21:01):

See also https://github.com/coq-community/manifesto/wiki/Continuous-Integration-with-Nix#alternative-setup-and-comparison

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

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

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

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

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

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

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 16:07):

@Théo Zimmermann the wiki says Nix uses OCaml 4.06.1, is that stale?

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

view this post on Zulip Théo Zimmermann (Sep 24 2020 at 17:23):

So 4.09.

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

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

view this post on Zulip Théo Zimmermann (Sep 24 2020 at 17:31):

See also https://docs.gitlab.com/ee/ci/multi_project_pipelines.html#creating-multi-project-pipelines-from-gitlab-ciyml

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

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

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

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

view this post on Zulip Gaëtan Gilbert (Sep 25 2020 at 19:19):

what does configure say for you locally?

view this post on Zulip Gaëtan Gilbert (Sep 25 2020 at 19:19):

and what coq commit?

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

view this post on Zulip Gaëtan Gilbert (Sep 25 2020 at 19:58):

just remove the default repo and use the online one instead

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

view this post on Zulip Théo Zimmermann (Sep 26 2020 at 11:22):

The zarith version is the right one.

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

view this post on Zulip Théo Zimmermann (Sep 27 2020 at 09:28):

"base" is the name of the image itself, I was not talking about the tag.

view this post on Zulip Beta Ziliani (Sep 27 2020 at 19:34):

Thanks guys. Now we are facing a different issue now (bors being dead).


Last updated: Oct 16 2021 at 02:03 UTC