fix: Adapt to PR coq-community/docker-coq#47

[erikmd]

Can be merged and released after coq-community/docker-coq#7 is deployed

This is a backward-compatible migration, so if there were no new release of the action, coq-community/docker-coq-action@v1.2.2 will continue to work as is with existing configurations until December 14, since Docker-Coq's "default tags" (which don't specify an ocaml version) will be retained as dual-switch up to December 14.

Edit: Adapt to coq-community/docker-coq#47

[Zimmi48]

Oh, minimal is deprecated? This is a surprise to me.

[Zimmi48]

BTW, in the end there was no announcement yet for the change in Docker-Coq single-switch vs double-switch, right? Should the end of the transition period still be on Dec 14th then?

[erikmd]

@Zimmi48

BTW, in the end there was no announcement yet for the change in Docker-Coq single-switch vs double-switch, right? Should the end of the transition period still be on Dec 14th then?

Hi, I wanted to announce it yesterday, but I've been busy. Soon anyway.

And which migration period do you think it is reasonable? 7 days maybe?

Finally, if you agree with the "backward-compatible" solution we discussed just now, here is the plan:

• Continue to follow semantic versioning & Don't bump the docker-coq-action to v2
• Keep ocaml_version: "minimal" working, only deprecate it so that we can remove it when the v2 will land
• Add ocaml_version: "default" that does not hardcode an ocaml version but rely on the Docker-Coq default;
  that image will change at the end of the migration (e.g. coqorg/coq:8.12 is currently two-switch, but we will have coqorg/coq:8.12 = coqorg/coq:8.12-ocaml-4.07-flambda afterwards); from the point of view of docker-coq-action users, this will only change the "default ocaml version" for users that did not specify a given version (configurations with ocaml_version: "minimal" won't be impacted)
• Update the documentation accordingly.

Let me know if you are OK with this plan, and I'll implement it very soon in this PR :)

Finally, a suggestion regarding the deprecation of "minimal": we could also print a warning in the log to document this further.

[Zimmi48]

I agree with this plan. 7 days sound right.

Finally, a suggestion regarding the deprecation of "minimal": we could also print a warning in the log to document this further.

Yes, it makes sense for a deprecated field.

The question that remains to be decided if whether to deprecate but preserve the semantics of "minimal" or to deprecate and change its semantics at the same time (to be synonymous of "default").

The latter would not be strictly compatibility-preserving, but we can decide depending on the usages that were made of it.

I just reviewed the 8 usages found with: https://github.com/search?q=docker-coq-action+minimal+language%3AYAML&type=code

Most come directly from a generation from a previous version of the coq-community templates. Note that the coq-community template used an explicit "minimal" from May 1st, when it was introduced (coq-community/templates#26), to June 26th (coq-community/templates#59).

The only exceptions are:

• The configuration of dblib, which tests as many OCaml versions as possible, but since this is a pure Coq library, there is a PR open proposing to switch to standard template-based, single-OCaml-version testing (add meta.yml and generate README and CI configuration from templates dblib#11).
• The configurations of Proof General, Hierarchy Builder and Coq-Elpi, which all seem to be inspired by the templates.

Out of these, only Coq-Elpi is a plugin. It is currently tested with Coq 8.12 and OCaml "minimal". If the semantics of "minimal" change to mean "default" and thus the plugin is not tested against OCaml 4.05 anymore (but 4.07 instead), this could be seen as a problem by its author (@gares), though it is easy to replace this "minimal" by an explicit "4.05" in this particular case.

WDYT?

[erikmd]

Hi @Zimmi48, thanks for your comments.
Regarding the semantics of "minimal" (as I also proposed to introduce "default" and you agreed with this new value), I actually see two sensible choices:

• add the "minimal business logic" to keep supporting "the minimal supported version in Docker-Coq"
• or remove that value "minimal" (but I guess we both think it'd be better not to do it for v1)

Indeed, having a "minimal" option that does not match its intended semantics would look a bit confusing to me, and having two values minimal = default with the same semantics (even if one is deprecated) seems a bit redundant.

Anyway, I agree with your concern that there should be the least possible business logic / ad-hoc code in docker-coq-action to "compute" the desired version! but I guess this can be done in a somewhat "future-proof" way (without needing to update the action as soon as a Coq is released that has the same minimal supported ocaml version as that of the previous release), as long as we we don't bump to docker-coq-action v2...

[Zimmi48]

If you are not comfortable with minimal = default, I'm fine with keeping minimal with some specific business-logic for it.

[erikmd]

Hi @Zimmi48, just FYI the "minimal" deprecation warning is implemented (and I guess it's in line which part of this Thursday's discussion on promoting a better version than 4.05.0!)
to have a look on the final rendering, see the Annotations summary (the 2nd annotation) − or the GHA log itself
(as for the rest of the PR implem: soonish)

[Zimmi48]

I'm surprised it doesn't also appear in the files changes tab as the Coq annotations themselves: https://github.com/erikmd/docker-coq-github-action-demo/pull/8/files

Apart from this, LGTM.

[LasseBlaauwbroek]

I suspect that this PR may have been forgotten to be merged together with the single-opam-switch change. Since then, ocaml-version no longer has an effect. Is there a reason this is delayed? Thanks.

[LasseBlaauwbroek]

I now see that the single-switch change may have been expected to be backward compatible. However, I need to move from 4.09 to 4.10 due to this change, and the CI is not properly selecting the 4.10 image. See here for example: https://github.com/coq-tactician/coq-tactician-stdlib/runs/1554834940

[erikmd]

@LasseBlaauwbroek my bad… the fact that this PR has been delayed induced that ocaml_version was ignored for the newly avaialble swiches!
We cannot merge #39 just now because it leads to other changes (the deprecation of "minimal", the addition of "default", doc to be finalized) but I'll push an independent fix right away…

[erikmd]

Hi @LasseBlaauwbroek, the issue is fixed now in v1.2.3, thanks again for your report!

[LasseBlaauwbroek]

Thanks!

[erikmd]

@Zimmi48 could you proofread the docs part of this PR? (README.md and error messages only)

Here is the link to the rendered README.md (only the coq_version and ocaml_version sections changed).

Regarding the error messages 1 and 2, they can be seen, rendered, as GHA annotations:

I plan to merge this PR on next Monday 2022-06-20 and do a minor release.
Next, remove the deprecated value of "minimal" the week after, on 2022-06-27 AOE.

[erikmd]

FTR, it seems that all Docker-Coq images experience a coq reinstall at runtime… probably because of this change, so I'm going to rebuild all Docker-Coq images… Done ✔️

[erikmd]

FWIW, to date there's only two YAML configs that use "minimal":
https://github.com/search?q=docker-coq-action+minimal+language%3AYAML&type=code
so I'll open a PR to suggest replacing "minimal" with "4.05" after this PR is merged and released.

[erikmd]

Let's wait for a newest CI run, then I'll merge and release this important patch tonight.