Please pick the version you prefer for Coq 8.17 in Coq Platform 2023.03

[MSoegtropIMC]

The Coq team released Coq 8.17+rc1 on December 29th, 2022 and plans to release Coq 8.17.0 around March 7th, 2023.
The corresponding Coq Platform release 2023.03 should be released before April 14th, 2023.
It can be delayed in case of difficulties until June 30, 2023, but this should be an exception.

This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.17+rc1.

Coq Platform CI is currently testing opam package coq-serapi.8.17+rc1+0.17.1
from official repository https://coq.inria.fr/opam/extra-dev/packages/coq-serapi/coq-serapi.8.17+rc1+0.17.1/opam.

In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.

In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2023.03, please inform us as soon as possible and before March 21st, 2023!

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.17~2023.03+preview1 which already supports Coq version 8.17+rc1 and contains already working (possibly patched / commit pinned) Coq Platform packages.

In case you want to select a different version, 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#335

[ejgallego]

Hi @MSoegtropIMC , I'd like to release a new vesrsion once Coq 8.17 is released.

I have proposed a different organization of the Opam package setup in coq/opam#2442 which should helps towards removing this step for packages like SerAPI.

[MSoegtropIMC]

@ejgallego : Just a reminder that Coq 8.17.0 is released. As far as I can tell there is no updated opam package for coq-serapi yet.

[MSoegtropIMC]

@ejgallego : I just saw your PR on the opam repo. I will take your PR as local opam patch in Coq Platform and see if this works for me and if so gor for it in the beta.

[ejgallego]

Dear Michael, indeed I'd suggest to use the official coq-serapi opam package that was just released.

[ejgallego]

Note that I found a problem with newer serapi's failing to compile on windows due to file paths becoming too long!

That's unfortunate, and while it can be solved by renaming a directory, it seems still an issue in general for win support.

[MSoegtropIMC]

I just started to work on Windows - let me see into what issues I run.

[MSoegtropIMC]

Path length is likely the least problem - the main problem is that the MinGW repo is not updated any more - no dune.3.7.0, not coq.8.17.0, ... I can only live on Windows cause of the Coq Platform local patch repo where I copy all these packages.

[ejgallego]

Yes that's a problem, maybe you could submit pull requests to https://github.com/ocaml-opam/opam-repository-mingw ?

Note that that repos already contains 4.14.1 for example.

[ejgallego]

I understand you are aware of https://discuss.ocaml.org/t/sunsetting-opam-repository-mingw/11632 ?

[ejgallego]

I generate the windows binaries using github CI + that repos, and they work kinda fine; modulo some fine tuning.

[MSoegtropIMC]

@ejgallego : I shortened the path and serapi now just so works (4 chars extra with the default path). I add a test on the root path length and work with the OCaml team to remove unnecessary restrictions.

I close this issue.

For the records: I am using coq-serapi.8.17.0+0.17.0 in the 8.17 pick of Coq Platform 2023.03.

And thanks for the pointer to the new MinGW repo - this info came after I decided what to do on Windows for the 2023.03 release. I will try to update to the new repo.

[ejgallego]

Thanks @MSoegtropIMC , I'm glad to hear that path shortening did work. It is a very annoying patch to carry but on the other hand it is easy to address.

Do you have an upstream OCaml issue about the path length limitation?