docker pull coqorg/coq:dev fails

mattam82 commented 2 years ago

Currently, I don't know why: coqorg/coq:dev-ocaml-4.07-flambda also fails, but one can get coqorg/coq:dev-ocaml-4.12-flambda

mattam82 commented 2 years ago

The error is:

Error response from daemon: manifest for coqorg/coq:dev not found: manifest unknown: manifest unknown

Alizter commented 2 years ago

AFAIK this has been happening for a while. The workaround is to use the flmabda version as you said.

proux01 commented 2 years ago

Well, Coq master doesn't compile anymore with OCaml 4.07 since it now requires OCaml >= 4.09. The dev images needs to be updated.

erikmd commented 2 years ago

Hi @mattam82 @Alizter @Zimmi48 @proux01 @palmskog @gares (sorry if I forget usernames)

Indeed, thanks for opening this issue.

To give more feedback: up to now, all docker-coq tags not specifying an ocaml version, like coqorg/coq:8.15 or coqorg/coq:dev:

were bundling two different ocaml switches (typically 4.05.0 and 4.07.1+flambda) by default.

(This was the choice made very earlier, when we devised of the architecture of docker-coq images with @ejgallego and @Zimmi48, but it appeared later on that indeed, it is much simpler and efficient to have 2 different images and pull 1 of them, rather than pulling a bigger image and doing opam switch STH inside. But this choice had been kept partially, for compatibility.)

With the recent end-of-support by coq master for both 4.05.0 and 4.07.1, keeping coqorg/coq:dev available did not make sense anymore w.r.t. the continuous deployment.

So I removed them, in favor of e.g.:

which are still continuously updated at each PR merged in master.

But definitely, the plan is to make such a "short tag" (also known as "default docker-coq tag") available anew for coqorg/coq:dev, with a single switch, for an appropriate ocaml version (the ocaml version chosen in Coq platform for instance), and likewise (for uniformity) for all docker-coq tags.

This requires a non trivial refactoring of images.yml specs and Dockerfile (and it needs to be propagated to mathcomp images and proofgeneral images), which explains why, by lack of time, I wasn't able to do this right away when coq's ocaml-4.07 end-of-support patch was merged.

Anyway, I implemented a large part of it today, and I hope to have all this going live for Monday 🤞, then ideally adding some automation ✨ (to e.g. receive an automatic notification when a new ocaml version is released, impacting docker-coq w.r.t. its ocaml-version policy that had been documented in the wiki).

I'll post anew in this issue when there's some news ^^

erikmd commented 2 years ago

The PR that solves this is now merged, and the corresponding pipeline is on-going:

~https://gitlab.com/coq-community/docker-coq/-/pipelines/562743090~ (parent pipeline) https://gitlab.com/coq-community/docker-coq/-/pipelines/562745107 (generated child pipeline)

Once it is completed (in ~30'), docker pull coqorg/coq:dev should be OK anew (with 4.13.1+flambda).

Will check mathcomp images afterwards.

erikmd commented 2 years ago

Done, and FYI here is the contents of coqorg/coq:dev and coqorg/coq:latest now:

docker run --pull always -it --rm coqorg/coq:dev opam list

``` dev: Pulling from coqorg/coq Digest: sha256:ea081a18b9ce454c89b02131b714b8b8b7393404c11abe0bf9f9a49b421a56cf Status: Image is up to date for coqorg/coq:dev # Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-threads base base-unix base conf-findutils 1 Virtual package relying on findutils conf-gmp 4 Virtual package relying on a GMP lib system installation coq dev pinned to version dev at git+https://github.com/coq/coq#b7258c31fe740df94f8546f5c7865e55c1be2456 coq-bignums dev Bignums, the Coq library of arbitrary large numbers dune 3.2.0 pinned to version 3.2.0 num 1.4 pinned to version 1.4 ocaml 4.13.1 The OCaml compiler (virtual package) ocaml-config 2 OCaml Switch Configuration ocaml-option-flambda 1 Set OCaml to be compiled with flambda activated ocaml-variants 4.13.1+options Official release of OCaml 4.13.1 ocamlfind 1.9.1 pinned to version 1.9.1 opam-depext 1.2.1-1 Install OS distribution packages zarith 1.12 pinned to version 1.12 ```

docker run --pull always -it --rm coqorg/coq:latest opam list

``` latest: Pulling from coqorg/coq Digest: sha256:ea32accfcc73a0a1658adeab33d9a25b6a98df89e6079ade110b411bd43aefe1 Status: Image is up to date for coqorg/coq:latest # Packages matching: installed # Name # Installed # Synopsis base v0.14.0 Full standard library replacement base-bigarray base base-threads base base-unix base biniou 1.2.1 Binary data format designed for sp cmdliner 1.0.4 Declarative definition of command conf-findutils 1 Virtual package relying on finduti conf-gmp 4 Virtual package relying on a GMP l coq 8.15.2 pinned to version 8.15.2 coq-bignums 8.15.0 Bignums, the Coq library of arbitr coq-serapi 8.15.0+0.15.0 Serialization library and protocol cppo 1.6.9 Code preprocessor like cpp for OCa csexp 1.5.1 Parsing and printing of S-expressi dune 3.2.0 pinned to version 3.2.0 dune-configurator 3.2.0 Helper library for gathering syste easy-format 1.3.2 High-level and functional interfac num 1.4 pinned to version 1.4 ocaml 4.07.1 The OCaml compiler (virtual packag ocaml-compiler-libs v0.12.4 OCaml compiler libraries repackage ocaml-config 1 OCaml Switch Configuration ocaml-secondary-compiler 4.08.1-1 OCaml 4.08.1 Secondary Switch Comp ocaml-variants 4.07.1+flambda Official release 4.07.1, with flam ocamlfind 1.9.1 pinned to version 1.9.1 ocamlfind-secondary 1.9.1 Adds support for ocaml-secondary-c opam-depext 1.2.1-1 Install OS distribution packages parsexp v0.14.2 S-expression parsing library ppx_derivers 1.2.1 Shared [@@deriving] plugin registr ppx_deriving 5.2.1 Type-driven code generation for OC ppx_deriving_yojson 3.6.1 JSON codec generator for OCaml ppx_import 1.9.1 A syntax extension for importing d ppx_sexp_conv v0.14.3 [@@deriving] plugin to generate S- ppxlib 0.25.0 Standard library for ppx rewriters result 1.5 Compatibility Result module sexplib v0.14.0 Library for serializing OCaml valu sexplib0 v0.14.0 Library containing the definition stdlib-shims 0.3.0 Backport some of the new stdlib fe yojson 1.7.0 Yojson is an optimized parsing and zarith 1.12 pinned to version 1.12 ```

erikmd commented 2 years ago

FTR, these two images (like all other ones) are mono-switch. As a result, they are around 30% smaller:

docker-coq image	compressed size / Docker Hub	total size (§)
~`coqorg/coq:8.15.1` (dual switch)~	1.39 GB	4.5 GB
`coqorg/coq:8.15.2` (4.07.1+flambda)	979 MB	3.17 GB

(§) the total size (indicated by $ docker images) is the cumulative space taken up by the image and all its parent images, once they are pulled by a docker client, but it should be noted that pulling two similar images that share common layers will involve deduplication.

FWIW:

docker-coq image	compressed size / Docker Hub	total size
`coqorg/coq:dev` (4.13.1+flambda)	1.13 GB	2.88 GB

For the list of all available images, see https://hub.docker.com/r/coqorg/coq#supported-tags as usual.

erikmd commented 2 years ago

And just FYI, I've just updated the Docker-Coq wiki accordingly:

https://github.com/coq-community/docker-coq/wiki#ocaml-versions-policy

coq-community / docker-coq

docker pull coqorg/coq:dev fails #46