Please create a tag for Coq 8.20 in Coq Platform 2025.01

[MSoegtropIMC]

The Coq team released Coq 8.20.0 on September 3rd, 2024.
The corresponding Coq Platform release 2025.01 should be released before Jan 31st, 2025.
It can be delayed in case of difficulties until Feb 28th, 2025, but this should be an exception.

This issue is to inform you that to our (possibly a few days old) best knowledge the latest released version of your project (1.2.1) does not work with Coq 8.20.0.
We tried to remove version restrictions in opam files and possibly make or configure files, but this did not suffice.

Please note that in Coq Platform CI (unlike Coq CI) we test only released / tagged versions. Coq CI appears to test this project, but has some special handling for your project which makes it difficult to retrieve the commit it tests for your project.

Could you please create a tag and opam package, or communicate us any existing tag that works with Coq branch v8.20, preferably before Dec 31st, 2024?
In case we might have to delay the Coq Platform release cause of issues with your project, we would prefer to be informed about the situation as early as possible.

In case the tag and opam package are available before Dec 8th, 2024, it will be included in an early Coq Platform beta release of the for Coq 8.20.0.

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.20~2025.01 which already supports Coq version 8.20.0 and contains already working (possibly patched / commit pinned) Coq Platform packages.

Please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#449

[palmskog]

@MSoegtropIMC it's incorrect that coq-reglang.1.2.1 doesn't work with Coq 8.20.0, it works just fine and the opam repo reflects this.

What might be happening is that you have pinned MathComp 2.3.0, and coq-reglang.1.2.1 is not yet marked as compatible with it, due to just being released.

[MSoegtropIMC]

@palmskog : as I wrote I do version restriction relaxations before I create the tickets. This is not enough - like a few other packages coq-reglang suffers from the file name conflict in mathcomp 2.3.0:

$ opam switch CP.2024.10.1~8.20~2025.01
$ opam install coq-reglang.1.2.1
The following actions will be performed:
=== install 1 package
  - install coq-reglang 1.2.1

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
-> retrieved coq-reglang.1.2.1  (cached)
[ERROR] The compilation of coq-reglang.1.2.1 failed at "make -j4".

#=== ERROR while compiling coq-reglang.1.2.1 ==================================#
# context     2.2.0 | macos/arm64 | ocaml-option-flambda.1 ocaml-variants.4.14.2+options | https://coq.inria.fr/opam/released#2024-12-16 12:01
# path        ~/.opam-current+working-tests/CP.2024.10.1~8.20~2025.01/.opam-switch/build/coq-reglang.1.2.1
# command     ~/.opam-current+working-tests/opam-init/hooks/sandbox.sh build make -j4
# exit-code   2
# env-file    ~/.opam-current+working-tests/log/coq-reglang-34719-8157d6.env
# output-file ~/.opam-current+working-tests/log/coq-reglang-34719-8157d6.out
### output ###
# [...]
# COQC theories/dfa.v
# COQC theories/nfa.v
# COQC theories/minimization.v
# File "./theories/minimization.v", line 5, characters 0-82:
# Error: Required library path matches several files in path (found
# /Users/msoegtrop/.opam-current+working-tests/CP.2024.10.1~8.20~2025.01/lib/coq/user-contrib/mathcomp/analysis/homotopy_theory/path.vo and
# /Users/msoegtrop/.opam-current+working-tests/CP.2024.10.1~8.20~2025.01/lib/coq/user-contrib/mathcomp/ssreflect/path.vo).
# 
# make[2]: *** [theories/minimization.vo] Error 1
# make[2]: *** Waiting for unfinished jobs....
# make[1]: *** [all] Error 2
# make: *** [all] Error 2

<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-reglang 1.2.1
+- 
- No changes have been performed

[palmskog]

@MSoegtropIMC to me this problem is unrelated to RegLang. From mathcomp Require Import path. has been the idiom to get path.vo from mathcomp.ssreflect for 10+ years. You can probably find many, many more breakages in Platform and non-Platform packages if you install coq-mathcomp-analysis. I think the proper solution to this is not to conflict all of these (possibly hundreds of) packages with coq-mathcomp-analysis, but rather that there is a new release of coq-mathcomp-analysis with the fix in math-comp/analysis@f788745

cc: @affeldt-aist

[MSoegtropIMC]

@palmskog : I meanwhile got the confirmation from mathcomp-analysis that this issue will be fixed by the end of the year, so this is fine - no fix for reglang is needed.

My post was also a reaction to your initial answer that reglang compiles fine. As this shows, this can depend on the installation of unrelated packages. If this is than an issue in the package producing the conflict or in the package doing not so specific requires needs to be discussed. The point of these tickets is to inform that there is an issue, which needs to be fixed in one way or another.

But I will improve the message stating that it is not compatible with the current state of the Coq Platform pick for Coq X.Y which can be found here ...

[palmskog]

I think there is a big difference between:

• this package can be successfully installed using opam using a fresh installation of Coq 8.X.Y (plus coq-mathcomp-ssreflect) - this is easily testable in CI, and in particular it's tested in the Coq opam archive CI
• this package can be successfully installed on current Platform pick, where there may be interference from many other packages/tools - this would need maintainers to use Platform CI for testing

[palmskog]

I think the point is that as an individual maintainer, one can and should be expected to solve "fresh installation" issues, but interference issues must usually be escalated to (Platform) ecosystem level - it's typically too much for the maintainer to figure out.

[MSoegtropIMC]

Well but this is a Platform ecosystem level issue which should be clear by the subject. It also explicitly says that the issue occurs in Coq Platform CI. So I don't see the point of nit picking on the wording. I think you know quite well what is meant.

But as I said I agree that the wording can be improved and will do so in the future. Note that the wording of the issue depends on a quite a few conditions and is put together from text blocks using a shell script. IMHO it is not that bad for this and reasonably informative.

[MSoegtropIMC]

I enabled coq-reglang.1.2.1 in Coq Platform via coq/platform#454 - it compiled fine with mathcomp-analysis.1.8.0 => closing.