search

mit-plv / coqutil

Coq library for tactics, basic definitions, sets, maps
MIT License
42 stars 24 forks source link

Please pick the version you prefer for Coq 8.16 in Coq Platform 2022.09 #71

Closed MSoegtropIMC closed 1 year ago

MSoegtropIMC commented 2 years ago

The Coq team released Coq 8.16+rc1 on June 01, 2022. The corresponding Coq Platform release 2022.09 should be released before September 15, 2022. It can be delayed in case of difficulties until October 15, 2022, 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.16+rc1.

Coq Platform CI is currently testing opam package coq-coqutil.0.0.1 from official repository https://coq.inria.fr/opam/released/packages/coq-coqutil/coq-coqutil.0.0.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 2022.09, please inform us as soon as possible and before August 31, 2022!

The working branch of Coq Platform, can be found here main. It contains package pick ~8.16+rc1~2022.09~preview1 which already supports Coq version 8.16+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: https://github.com/coq/platform/issues/274

MSoegtropIMC commented 2 years ago

@samuelgruetter @andres-erbsen @JasonGross : can you please confirm that this is the version you want to see in Coq Platform 2022.09?

Or should I remove it since bedrock2 anyway won't make it in 2022.09 since I am not sure we can fix the cross platform issues in a week or two.

andres-erbsen commented 2 years ago

I checked that the tested branch builds on 8.16 and created https://github.com/mit-plv/coqutil/releases/tag/2022-09 I have no opinion on whether it should be included in Coq platform, but it is probably no worse than any older version.

samuelgruetter commented 2 years ago

If I understood correctly, the Coq Platform should contain only (reasonably) stable packages that are ready to be used by a broader audience, and I think coqutil/bedrock2 hasn't reached that stage yet. I think that providing a beginner-friendly, well-documented Coq Platform is a great thing to do, but I'm a bit uncomfortable with the idea that newcomers using the Coq Platform will run into issues with coqutil/bedrock2 and get a bad impression of Coq as a whole because of that. So in my opinion, it would be better to exclude coqutil/bedrock2 from the Coq Platform for the time being.

MSoegtropIMC commented 2 years ago

@samuelgruetter : There is a request to include Fiat Cryptography in Coq Platform here (https://github.com/coq/platform/issues/178) which require coq-coqutil. There was some discussion there.

Actually I must admit I am not sure why I concluded that bedrock2 is also required - I guess it was the comment of @JasonGross here: https://github.com/coq/platform/issues/178#issuecomment-1074633687.

Coq Platform has an "extended level" which is more of a playground for the curious. Unlike projects in the full level there is no guarantee that there won't be a lot of breaking changes in every release or that it won't be removed. The extended level is more about making it easy for smart students to "play" with it. Experts in a project frequently underestimate the difficulties most outsiders have to install stuff, so installation issues likely reduce the audience quite a bit. And in my experience students which are good at Coq are not necessarily best friend with all the involved build technology.

Let's continue the discussion what makes sense in the issue I mentioned above. This is your decision - I am only taking actions cause of the above request and the comment by @JasonGross.

MSoegtropIMC commented 2 years ago

I am about to create the Coq Platform beta for 8.16 (2022.09).

What is the final verdict for including coqutil? Should we delay it until fiat-crypto and/or bedrock2 are included?

MSoegtropIMC commented 1 year ago

This topic has been discussed in (https://github.com/coq/platform/issues/178). fiat-crypto and coqutil are included in Coq Platform 2022.09. The coq-coqutil version pickes is 0.0.2 - the only version compatible with fiat-crypto.

So I am closing this as solved.