Please create a tag 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 to our (possibly a few days old) best knowledge the latest released version of your project (1.6.4) does not work with Coq 8.17+rc1.
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 is currently testing commit 81d8ffe on repository https://github.com/QuickChick/QuickChick - which likely means that this commit does work in Coq CI.

Could you please create a tag and opam package, or communicate us any existing tag that works with Coq branch v8.17, preferably before March 21st, 2023?
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 March 21st, 2023, it will be included in an early Coq Platform beta release of the for Coq 8.17+rc1.

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.

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

[MSoegtropIMC]

@lemonidas @catalin-hritcu @zoep : I would appreciate a status update and/or ETA on this.

[Lysxia]

@lemonidas Should we aim to get 2.0 ready for this Coq platform release (the library is buildable now but maybe we want to make sure that it works with tutorial/ and the QC book?), or should I just make a minor release with the current master branch?

[lemonidas]

Let's push for a 2.0 release - if the only thing failing are the proof derivations we can comment them out until we get around to them.

[MSoegtropIMC]

May I ask if there is a status update and/or an ETA?

[MSoegtropIMC]

@Lysxia @lemonidas : please note that this the only Coq Platform "full"-level package for which I don't yet have an ETA for a 8.17 compatible release. The only other "full-level" package without a 8.17 release is MetaCoq, for which I have an ETA of this week.

I would like to create a Coq Platform 2023.03 beta today or tomorrow - my current status is that I have to remove QuickChick in the beta release. Since you noted above that you plan to do a new major release, it does not make a lot of sense to include a master commit into the beta.

[MSoegtropIMC]

@Lysxia @lemonidas : I saw your opam PR coq/opam#2548 - I guess 1.6.5 is the version which shall go into the Coq Platform release, but I would appreciate if you could confirm this here (the Coq Platform rules say that the version picks are discussed with the authors / maintainers).

[liyishuai]

I as a co-maintainer would take the responsibility and recommend including 1.6.5 in the Coq platform release.
Please follow Leo's suggestion.

[lemonidas]

We should have a 2.0 release by the end of the day though.

[MSoegtropIMC]

Very well - I am happy to wait for 2.0 then.

That's the exact reason for having these discussion issues - to not pick 1.6.5 when there is 2.0 the next day.

[lemonidas]

Feel free to use this release: https://github.com/QuickChick/QuickChick/releases/tag/v.2.0

Will make the opam PR soon.

[MSoegtropIMC]

Thanks! I Updated the 8.17 pick in Coq Platform 2023.03 to coq-quickchick.2.0.0 and close this issue.

[MSoegtropIMC]

@lemonidas : unfortunately I get reproducibly this error on Windows with 2.0.0:

File "src/dune", line 1, characters 0-92:
1 | (coq.theory
2 |  (name QuickChick)
3 |  (package coq-quickchick)
4 |  (libraries coq-quickchick.plugin))
Error: No rule found for
src/C/bin/cygwin64_coq_platform/home/Michael/.opam/CP.2023.03+b1~8.17~2023.03+beta1/.opam-switch/build/coq-quickchick.2.0.0/_build/install/default/lib/coq-quickchick/META

I don't know enough about dune to have any idea where this comes from. But I can say that when the build is finished the file does exist.

[MSoegtropIMC]

I just tested 1.6.5 and this does work fine, so I will switch back to 1.6.5 (on all platforms) for the time beeing.

[Lysxia]

I'm not sure how to troubleshoot that error off the top of my head either. 1.6.5 seems like the best workaround for the moment.

[MSoegtropIMC]

Confirming that I used 1.6.5 and closing.