feat: Bump COMPILER_EDGE to 4.09.0+flambda

[liyishuai]

Resolves #4

[liyishuai]

Is it worth rebasing our image on top of ocaml/opam2?

[erikmd]

@liyishuai

Is it worth rebasing our image on top of ocaml/opam2?

No I don't think so. The main motivation of this design choice of coqorg/base (that had been discussed with @Zimmi48 and @ejgallego) was to provide only two switches: roughly, the minimal version of OCaml supported by Coq = 4.05.0, and a more recent one with +flambda.

And it happens ocaml/opam2 provides many more switches ocaml-base-compiler.*, which has a strong impact on the size of the image:

$ docker run --rm -it coqorg/base opam switch
#   switch          compiler                       description
->  4.05.0          ocaml-base-compiler.4.05.0     4.05.0
    4.07.1+flambda  ocaml-variants.4.07.1+flambda  4.07.1+flambda

$ docker run --rm -it ocaml/opam2 opam switch
#   switch  compiler                    description
    4.02    ocaml-base-compiler.4.02.3  4.02
    4.03    ocaml-base-compiler.4.03.0  4.03
    4.04    ocaml-base-compiler.4.04.2  4.04
    4.05    ocaml-base-compiler.4.05.0  4.05
    4.06    ocaml-base-compiler.4.06.1  4.06
    4.07    ocaml-base-compiler.4.07.1  4.07
    4.08    ocaml-base-compiler.4.08.1  4.08
    4.09    ocaml-base-compiler.4.09.0  4.09
->  4.10    ocaml-base-compiler.4.10.0  4.10

$ docker images | grep -e ocaml/opam2 -e coqorg/base
ocaml/opam2    latest    04fb66816491    11 days ago    3.55GB
coqorg/base    latest    3c4f714b60b9    7 weeks ago    1.04GB

[ejgallego]

Hi folks, note that OCaml >= 4.08 did introduce some non-trivial performance regression (c.f. ocaml/ocaml#9326) so indeed I dunno if you should wait a bit before the bump.

[liyishuai]

The reason I proposed this bump is that Software Foundations' CI uses coqorg/coq, and a recent change depends on OCaml >= 4.08. If we are to upgrade OCaml eventually, perhaps no need to wait for the performance issue to be fixed.

[ejgallego]

Yup, I understand it is very convenient to have 4.09, I dunno; the OCaml problem is really unfortunate, maybe the 3 versions should be kept if moving away from 4.07 is gonna impact some users with heavy developments?

[liyishuai]

maybe the 3 versions should be kept if moving away from 4.07 is gonna impact some users with heavy developments?

Good idea. Should we have:

• COMPILER="4.05.0"
• COMPILER_EDGE="4.09.0+flambda"
• and a 4.07.1+flambda switch referenced by some variable (or no variable)?

[erikmd]

maybe the 3 versions should be kept if moving away from 4.07 is gonna impact some users with heavy developments?

Good idea. Should we have:

* `COMPILER="4.05.0"`

* `COMPILER_EDGE="4.09.0+flambda"`

* and a `4.07.1+flambda` switch referenced by some variable (or no variable)?

@ejgallego @liyishuai I agree with your two concerns (that 4.07.1+flambda is not "edge" anymore and that 4.09.0(+flambda) could impact heavy developments), but I somewhat disagree with your intermediate solution − of adding a third switch:

• Indeed, that would readily increase the build time and the size of coqorg/coq:{8.7, 8.8, 8.9, 8.10, 8.11, dev} images of around 50%, which is not negligible at all.
• Moreover if we take into account the Docker Hub workers specifications/limitations that had been mentioned in this page, a regular build of a coqorg/coq:dev image currently takes around 90' on Docker Hub, while adding 50% of compilation time would maybe not scale.
• Finally I'm unsure that intermediate solution would bring a clear benefit for coqorg/coq users, w.r.t. the previously mentioned downsides (build time / image size). E.g., the default switch enabled by default in the images is 4.05.0.

[erikmd]

So I have an alternative proposal, similar to what @liyishuai suggested (If we are to upgrade OCaml eventually, perhaps no need to wait for the performance issue to be fixed.):

• we could delay the merge of this PR feat: Bump COMPILER_EDGE to 4.09.0+flambda #5 of one week,
• and post a message on coq-club mentioning that we are considering replacing the 4.07.1+flambda switch with 4.09.0+flambda in coqorg/coq on March 14, that this will be convenient to have a pre-compiled Coq with a much more recent OCaml, but that a performance issue has been identified with 4.09.0 (@ejgallego IIRC only tested without flambda, so maybe 4.09.0+flambda wouldn't be impacted?) and asking if users relying on coqorg/coq's 4.07.1+flambda switch would have some feedback/objection/suggestion?

WDYT?

[ejgallego]

Size is indeed a concern, on the other hand the issue with OCaml is serious enough as to block the upgrade IMO. We are talking of increased compilation times of 12/15% that we could measure, that seems like a lot to me.

I can only think of two choices:

• keep 4.07.1 for now, and hope that OCaml 4.11 does fix the regression
• restructure the images so only one OCaml compiler is shipped by image, I'm unsure about this solutions [and moreover seems like a lot of work], but we could then have coq:4.05.0+dev (or coq:dev+4.05.0 etc...?

[erikmd]

@ejgallego

I can only think of two choices:

• keep 4.07.1 for now, and hope that OCaml 4.11 does fix the regression

looks reasonable to me, except that this will hinder @liyishuai's use case to benefit from coqorg/coq images with OCaml 4.08.0

BTW @liyishuai could you post a link to the Software Foundations' repo so that this thread is self-contained? Also, can you confirm which versions of Coq you'd like to test with this recent version of OCaml?

• restructure the images so only one OCaml compiler is shipped by image, I'm unsure about this solutions [and moreover seems like a lot of work], but we could then have coq:4.05.0+dev (or coq:dev+4.05.0 etc...?

this would be a large refactoring, obviously non-backward-compatible for the users of the docker-coq images so I'm a bit split on this; maybe this is the way to go, or maybe we need to think about a similar solution, e.g. preserving all images containing two switches, and adding extra images coqorg/coq:dev-4.09 (as an aside, + is not allowed in the Docker image tags but - is) with just one switch 4.09.0+flambda? maybe that looks a bit weird, maybe one such solution should be considered as a temporary solution before switching to 4.11, but in any case we have to further discuss this…

(I also Cc @Zimmi48 @SkySkimmer in case they have suggestions about that non-trivial choice)

[liyishuai]

BTW @liyishuai could you post a link to the Software Foundations' repo so that this thread is self-contained?

Software Foundations is maintained in a private repository because the authors haven't decided to publicise solutions to exercises. The changes that require OCaml >= 4.08 are in the tools for building the textbook.

Also, can you confirm which versions of Coq you'd like to test with this recent version of OCaml?

8.8, 8.9, 8.10, dev.

[liyishuai]

• restructure the images so only one OCaml compiler is shipped by image, I'm unsure about this solutions [and moreover seems like a lot of work], but we could then have coq:4.05.0+dev (or coq:dev+4.05.0 etc...?

this would be a large refactoring, obviously non-backward-compatible for the users of the docker-coq images so I'm a bit split on this; maybe this is the way to go, or maybe we need to think about a similar solution, e.g. preserving all images containing two switches, and adding extra images coqorg/coq:dev-4.09 (as an aside, + is not allowed in the Docker image tags but - is) with just one switch 4.09.0+flambda? maybe that looks a bit weird, maybe one such solution should be considered as a temporary solution before switching to 4.11, but in any case we have to further discuss this…

We can first add some new tags (immediately), and announce that existing tags are subject to changes (that may alias to the added tags) in the future.

[erikmd]

Thanks to @ejgallego's feedback regarding the performance hit with OCaml >=4.08.0, I believe we could close that PR for the moment and continue the discussion in the issue #4 to find some solution