[external issue] compilation error using coqorg/coq:dev with opam unpin coq; opam upgrade

[liyishuai]

https://circleci.com/gh/liyishuai/QuickChick/116

### output ###
# File "dune", line 5, characters 14-25:
# 5 |  (public_name coq-bignums)
#                   ^^^^^^^^^^^
# Warning: (public_name ...) is deprecated and will be removed in the Coq
# language version 1.0, please use (package ...) instead
#         coqc BigNumPrelude.vo (exit 1)
# (cd _build/default && /home/coq/.opam/4.05.0/bin/coqc -I /home/coq/.opam/4.05.0/lib/coq/clib -I /home/coq/.opam/4.05.0/lib/coq/config -I /home/coq/.opam/4.05.0/lib/coq/engine -I /home/coq/.opam/4.05.0/lib/coq/gramlib/.pack -I /home/coq/.opam/4.05.0/lib/coq/interp -I /home/coq/.opam/4.05.0/lib/coq/kernel -I /home/coq/.opam/4.05.0/lib/coq/kernel/byterun -I /home/coq/.opam/4.05.0/lib/coq/lib -I [...]
# File "./BigNumPrelude.v", line 28, characters 0-42:
# Error: Dynlink error: interface mismatch on Vernacexpr

[ejgallego]

This seems like a problem with stale files in opam / your CI setup; hard to debug more. Seems to work fine here.

[liyishuai]

Indeed, works on my local machine.

[ejgallego]

Likely a problem with the coq.dev package tho, so maybe worth opening an issue in the coq opam repository? I'm unsure how reliable the current coq.dev packages are.

[liyishuai]

I've just upgraded coq.dev on my machine, and coq-bignum.dev seemed working. Still trying to locate the error.

[liyishuai]

Hmm it's Docker-specific: ocaml/opam#3997

[erikmd]

Hi @liyishuai, good catch: to sum up it indeed seems the error you got was (indirectly) caused by ocaml/opam#3997, because your CI script amounts to reinstall Coq and Bignums (see below), and due to the Docker/OPAM timestamps issue, the removal of installed opam libraries doesn't really work currently.

BTW, is there any reason why you added these two lines?
because at first sight, you're losing the benefit of having a pinned, prebuilt Coq in the first place…
(that's the reason why in the Travis CI template I only suggested to do opam update -y)

[erikmd]

(Also thanks @liyishuai for opening coq-community/docker-base#6 )

[liyishuai]

The reason was I wanted to upgrade Coq to the very latest version. When Coq developers submit a PR to coq-quickchick.dev, I don't want to wait for Docker image to upgrade coq.dev (currently nightly?) before checking against Coq master branch.

[erikmd]

@liyishuai

coq.dev (currently nightly?)

yes, coqorg/coq:dev is rebuilt every night from 00:00 Paris Time.
This is mentioned in the https://github.com/coq-community/docker-coq/wiki page, which also provides a badge to be able to check anytime what is the SHA1 of the Coq commit gathered in the coqorg/coq:dev image:

so yes a lag is possible if PRs have been merged since the morning, but unless the merged PRs at stake integrate a non-backward-compatible feature in Coq master (e.g. involving QuickChick overlays), I'd be tempted to say that this ~1-day lag wouldn't be that critical.

If this is an issue, I understand why you considered doing this manual opam upgrade, but maybe you could refactor your first step, so that if the SHA1 of Coq (see below) is unchanged w.r.t. the result of opam pin list, you could just skip that step?

(because I'm afraid your current configuration will always recompile Coq+bignums due to the git-unpinning, even if the image is already up-to-date)

How to get the latest SHA1 of Coq master

COQ_BRANCH="master"
COQ_COMMIT=$(curl -fsL -X GET -H "Accept: application/vnd.github.v3.sha" https://api.github.com/repos/coq/coq/commits/${COQ_BRANCH})
echo $COQ_COMMIT

(cf. https://github.com/coq-community/docker-coq/blob/dev/hooks/build#L15-L18 )

[ejgallego]

Actually @erikmd that is a functionality that could be provided by the docker image itself? Like setting "LASTEST_COQDEV` would mean the coq build is refreshed?

[At some point we could indeed push a layer for each Coq commit?]

[liyishuai]

[At some point we could indeed push a layer for each Coq commit?]

Since coqorg/coq is built on Docker Hub, we can trigger builds upon pushes to Coq master branch with a webhook.

[erikmd]

Thanks for your comments!

Actually we already discussed this suggestion once or twice (I didn't find again the issue number so maybe it was on gitter), and someone had proposed for example to switch to 2-automated builds per day, but we finally decided to keep the workflow as is.

I don't say one such evolution is not desirable, I just say that the current architecture is a trade-off regarding the possible lag between coqorg/coq:dev and coq@master and the scalability of the infrastructure (in particular, Docker Hub only provides one worker per organization, and compiling coqorg/coq:dev on Docker Hub takes more than 90', so that even if we were adding an automatic HTTPS request to trigger a rebuild for that image for each PR merge in coq@master, there will be a non-negligible lag).

but I guess the discussion starts going beyond this issue #36 😃 (which is BTW addressed by @liyishuai's PR coq-community/docker-base#6 with the OPAMPRECISETRACKING="1" patch, that is being deployed in all coqorg/coq images, see this page for the build status and that page for exploring the environment variables in each tag),
so feel free to open another issue if you think we need to further discuss on the nightly builds

[ejgallego]

compiling coqorg/coq:dev on Docker Hub takes more than 90'

@erikmd , I'm unsure if to open an issue about more frequent builds yet; one quick question, does the 90' minutes mark include the time to setup the opam switches?

If yes, why isn't the Coq image reusing the OCaml build hashes?

[liyishuai]

why isn't the Coq image reusing the OCaml build hashes?

Discussed earlier in coq-community/docker-base#5 (comment), not certain if image sizes matter that much. I'd prefer reducing time to saving space.

[ejgallego]

I see, thanks. So 90' for buliding Coq twice seems like a lot of time, let me have a look.

[erikmd]

@liyishuai

I'd prefer reducing time to saving space.

I somewhat disagree here, as both criteria are important for me:

• regarding the time requirement: the overall aim of coqorg/coq images is precisely to speed-up the CI builds so that a prebuilt set of opam switches with Coq already installed is readily available (BTW as I said earlier this time-saving advantage is partly lost if you do opam unpin coq; opam upgrade :)

if we want to update coqorg/coq:dev more frequently, the current approach (Docker Hub automated build) is "pull-based" and would not scale a priori if many Coq PRs are merged in a row, so IMO another proper solution would be a "push-based" approach by adding a dedicated deploy job inside the GitLab CI pipeline of Coq so that it docker-push to Docker Hub (like what I implemented for mathcomp.dev); so this is feasible but can have an impact on the nightly build of mathcomp/mathcomp:*-coq-dev and mathcomp/mathcomp-dev:coq-dev: I mean, if the nightly build of those two mathcomp images is kept as is (less frequent than coqorg/coq:dev) it may sound less consistent; at the very least the frequency difference should be documented.

• regarding the size requirement: the overall guidelines when maintaining Docker images precisely recommends to reduce their size as much as possible, and more specifically when distributing multi-purpose images (that can be used in a CI context as well as on a local workstation, we have to be careful not to increase this size significantly if another solution is possible, and I think so)

[erikmd]

@ejgallego

I'm unsure if to open an issue about more frequent builds yet;

Actually I realize this issue does not deals with bignums but only with docker-base, so if you don't object I will transfer that issue to https://github.com/coq-community/docker-base/issues

[erikmd]

@ejgallego

does the 90' minutes mark include the time to setup the opam switches?

No, because the first step done by the docker-coq image is to pull a docker-base image.

Actually it should be noted that the timing obtained in Docker Hub is strongly dependent on the infrastructure provided for its works, which seems significantly less efficient than Gitlab CI workers, in particular as mentioned in the following doc that I assume up-to-date:

https://forums.docker.com/t/automated-build-resource-restrictions/1413

The current limits on Automated Builds are:
2 hours
2 GB RAM
1 CPU
30 GB Disk Space

so even if I added some -j 2 flag in the underlying Dockerfile, compiling Coq in the two switches in the Docker Hub environment could be more costly in terms of elapsed time than on a personal workstation (I didn't re-test this but this is my intuition)

[ejgallego]

The current limits on Automated Builds are:

That's the information I was looking for and I couldn't find, thanks @erikmd

[Zimmi48]

@liyishuai Note that if you're looking to work around this nightly build issue, you may be interested in the Nix solution that the coq-community templates also support. When using the coq-on-cachix repo, you have assurance that the version you test is pre-built but it can still be lagging behind (but usually not much). If you use the normal repo instead, Coq might need to be rebuilt but it will be always up-to-date.

[erikmd]

@Zimmi48 yes! but I believe the coq-on-cachix builds currently rely on OCaml 4.06.1 while @liyishuai was especially interested in OCaml >= 4.08.0 IIRC

[liyishuai]

Checking against cutting-edge Coq is required by QuickChick CI, for Adapt to Coq PRs. QuickChick works fine on 4.06.1, I'll take a look at the coq-on-cachix approach.
Software Foundations calls for OCaml >= 4.08 but can live with not-so-new coq.dev, so not too urgent for coq-on-cachix to upgrade OCaml.

---

Side comment: macOS Catalina users can check out NixOS/nix#2925 (comment)

[erikmd]

OK @liyishuai ; but are you still interested in having coqorg/coq:*-ocaml-2.09 switches?

BTW note that it is possible to use both coqorg/coq and Nix in your CI, to benefit from a full-blown opam environment (namely, to test the "opam installability") and from a more recent coq.dev provided by Nix, see e.g. the templates' Travis CI conf file that uses both.

[liyishuai]

Yes upgraded OCaml is still helpful to building Software Foundations.