Please create a tag for Coq 8.17 in Coq Platform 2023.03

[MSoegtropIMC]

Please create a tag for Coq 8.17 in Coq Platform 2023.03

[lemonidas]

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

[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.

[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.