Feature wish: Add coq-serapi in docker-coq for Alectryon support

[erikmd]

Follow-up of issue cpitclaudel/alectryon#39 (opened by @Bruno-366)

Cc @cpitclaudel @Zimmi48 FYI

[erikmd]

Hi all, just to let you know, I'm currently working on this feature request, and to summarize the design that looked natural to me:

• Given that most of the documentation compilation time (as pointed out by @palmskog in PR coq-community/hydra-battles#59) is related to coq-serapi, and as alectryon may be updated more frequently than coq or serapi, I plan to merely integrate coq-serapi by default in all coqorg/coq images (that are compatible).
• So, end users could just do python3 -m pip install alectryon (if need be)
• Next, we'll be able to discuss (say, in this issue), to decide whether this latter python step should also be integrated somehow in docker-coq-action.
• But for the time being, users will be able to just rely on the after_script field, for example.

The preparation of the build is still on-going, so I'll comment further in this issue when it's deployed.

[palmskog]

@erikmd I'm personally delighted about the prospect of SerAPI and the tools provided by the coq-serapi package getting included by default in all official Docker images - not least for the proof engineering research potential.

Let me also ping in @ejgallego about this. Do you see any obstacles here, Emilio? Can we help out in some way to ensure SerAPI keeps getting successfully built with the various opam versions of Coq?

[cpitclaudel]

That sounds good to me!

[erikmd]

Thanks for your comments! so far, I've just done the upgrade in the docker-base registry — updating opam to the latest 2.0.x version, dune to the recently-released 2.9.1 and ocamlfind, num to the latest version as well.
(It requires a small refactoring of the Dockerfile as the opam switch create command for ocaml 4.12.0 has changed — it looks more flexible.)

Regarding @palmskog's remark

Can we help out in some way to ensure SerAPI keeps getting successfully built with the various opam versions of Coq?

I was just planning to rely, for each version of Coq, on the latest released coq-serapi, cf. these available versions in opam:

$ opam show coq-serapi

<><> coq-serapi: information on all versions ><><><><><><><><><><><><><><><><><>
name         coq-serapi
all-versions 8.7.1+0.4  8.7.1+0.4.1  8.7.1+0.4.2  8.7.1+0.4.8  8.7.1+0.4.12
             8.7.2+0.4.13  8.8.0+0.5.1  8.8.0+0.5.2  8.8.0+0.5.3  8.8.0+0.5.4
             8.8.0+0.5.5  8.8.0+0.5.6  8.9.0+0.6.0  8.9.0+0.6.1  8.10.0+0.7.0
             8.10.0+0.7.1  8.10.0+0.7.2  8.11.0+0.11.0  8.11.0+0.11.1
             8.12.0+0.12.0  8.12.0+0.12.1  8.13.0+0.13.0

I'll look at this next step ASAP.
(BTW, nothing would prevent us / @ejgallego to add more versions (if need be) in the opam-repository, then in the Docker images)

As an aside, note that given this requirement (using the coq-serapi package released in opam), it'll be straightforward to install coq-serapi in the stable Docker-Coq images;
but I'm wondering if we can make the choice (at least for now…) not to install coq-serapi in coqorg/coq:dev (unless you think this is useful for applications from now on? → in which case we could either add coq-serapi in extra-dev or use opam's git pinning); WDYT?

[Zimmi48]

@ejgallego doesn't continuously maintain compatibility with Coq dev, so unless he changes his process (and in this case, we should get SerAPI into Coq's CI), there is no way we can have SerAPI in coqorg/coq:dev.

[ejgallego]

Thanks for the update folks, I have done a quick write up of road map ideas at ejgallego/coq-serapi#252 , please feel free to comment / suggest.

@ejgallego doesn't continuously maintain compatibility with Coq dev, so unless he changes his process (and in this case, we should get SerAPI into Coq's CI), there is no way we can have SerAPI in coqorg/coq:dev.

I have mentioned this point in the above issue, indeed, would we merge the seralization part, it would be feasible to add serapi to Coq's CI IMVHO.

[Zimmi48]

Maybe that's something worth being discussed during the next Coq Call to have an update on everyone's opinions on this aspect.

[erikmd]

Hi all (Cc @cpitclaudel @ejgallego @palmskog @Zimmi48 @proux01 @CohenCyril FYI)
my first upgrade step (related to this issue) is completed, so I guess I can close the issue.

To sum up, while Alectryon's doc suggested installing "coq-serapi>=8.10.0+0.7.0" as a minimal version, I relaxed a bit the constraint so that (thanks to currently available versions of coq-serapi in opam), coq-serapi is now available in all images and switches such that:

• coq >= 8.8
• ocaml >= 4.07

− the detail of the changes on the Docker-Coq YAML spec are gathered in these two PRs:

• Add coq-serapi & Rebuild coqorg/coq:* to benefit from coqorg/base:* update #31
• fix(coqorg/coq:8.7*): coq-serapi is not coinstallable with coq 8.7 #33

FTR, the available images are listed in the Docker Hub description.

And beyond the addition of coq-serapi, the current images incorporate these updates:

• Support for ocaml 4.12 (for coq ∈ {8.13, dev})
• ocaml patchlevel bump: {4.10.1→4.10.2 ; 4.11.1→4.11.2}
• dune version bump: 2.8.5→2.9.1 (latest)
• opam patchlevel bump: 2.0.8→2.0.9
• num patchlevel bump: 1.3→1.4
• ocamlfind version bump: 1.8.1→1.9.1

[erikmd]

FTR the next three steps for docker-coq are:

1. Add coqorg/coq:8.14* (with autobuild from the branch, to ease CI tests before 8.14 release) done
2. Keep-but-deprecate 4.05.0 as the "default" ocaml version in some switches (by "default" version, I just mean if the ocaml version is unspecified in the Docker image tag: because each Coq version already comes with 4 versions of OCaml, which are easily/directly available with a coqorg/coq:8.*-ocaml-* suffix, e.g. coqorg/coq:8.13-ocaml-4.12-flambda)
   → this is related to Which default OCaml version for the images #30
3. Propagate the previous items to docker-mathcomp done