PrincetonUniversity/VST

Informative: pick of tag for upcoming release of Coq Platform for Coq 8.14

Closed this issue · 5 comments

The Coq team released Coq 8.14+rc1 on September 17, 2021
and plans to release Coq 8.14.0 before October 31, 2021.
A corresponding Coq Platform releases should be released before November 30, 2021.
It can be dealyed in case of difficulties until January 31, 2022, but this should be an exception.

This issue is to inform you that your latest tag does work fine with Coq 8.14+rc1.

Coq Platform currently uses the opam package 'coq-vst.2.8~flex'
from platform patch repository https://github.com/coq/platform/tree/main/opam/opam-coq-archive/extra-dev.

Note: We had to patch the opam package and possibly the make file to accept the new version of Coq, but no other changes were required.

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

In case you would prefer to see an updated version in the upcoming Coq Platform, please inform as as soon as possible!

Thanks!

P.S.: this issue has been created semi-automatically.

CC: coq/platform#139

@andrew-appel : can you please close this issue if coq-vst.2.8 is the version you want to see in Coq Platform 2021.11?

Actually, I have a question: Which version of CompCert will be in Coq Platform 2021.11? Will it be 3.9 or 3.10? @xavierleroy

I think it's CompCert 3.9, because 3.10 is not yet released (but soon!) and breaks VST and perhaps other components.

Yes my current plan is 3.9. This has been discussed here: (AbsInt/CompCert#414).

Btw.: the Coq Platform meta ticket for all version picking discussions is linked above.

One more note: Coq Platform now allows multiple package picks, so publishing updated picks between Coq releases is much more light weight than it used to be. We likely won't have signed installers for all picks, but it will still be easy to install using the scripts. It still needs to be found out what makes sense, but I think adding updated picks every 2 or 3 months is not unrealistic - the Coq ecosystem has become quite dynamic. I think this should reduce the need to squeeze in new versions in a hurry.