2022.01 track creation for coq-prover

store-requests
1

Hello, we are about to release a new version of the Coq prover and we’d like to open a track called 2022.01.

Best regards

2

Per Process for aliases, auto-connections and tracks , we need a 1-week voting/discussion period, so I’ll check back on the discussion and votes in a few days.

I have three questions before casting my vote.

  1. What’s coq-prover’s release cadence, how often is a new major version (potentially requiring a new track) released? is this documented somewhere by upstream?
  2. Is there some commitment from upstream on maintenance of old versions? e.g. is 2021.09.0 and older still supported with security updates? will they continue to be supported once a new version is out, and for how long?
  3. Are new versions backwards-incompatible? meaning, if I was running 2021.09.0 and try to install 2022.01, will that just work, or do I need to migrate my data/configuration, or will things break horribly?

Thanks!

  • Daniel
3

Hi,

  1. The Coq proof assistant is released every six months in theory, and the Coq Platform (which is released through Snap as coq-prover) mostly follows this cycle, but there was a long delay producing the 8.14 version of Coq, which resulted in a 2021.09 version which was still based on Coq 8.13 (but with major updates of other libraries). The 2022.01 version will be based on Coq 8.14, and we expect a 2022.03 version based on Coq 8.15 (which was released just four months after Coq 8.14 because a lot of changes had accumulated). See https://github.com/coq/coq/wiki/Release-Plan for the release schedule of upstream Coq.

  2. There is no commitment to maintaining past releases when new ones have become available. The notion of security update doesn’t really apply to Coq, but mostly this is a question of manpower.

  3. Yes, new major versions are virtually always backward-incompatible. Things will often break when migrating to a new version, although not horribly: Coq gives error messages that are often sufficiently clear to understand what needs to be (manually) updated to make a Coq file work with the new version, and when that’s not sufficient, the releases notes are sufficiently detailed to help figure this out: https://coq.inria.fr/refman/changes.html

The necessity of using tracks really comes from this last point, combined with the auto-update feature of Snap. For new learners, using the default track and being auto-updated to a new major version will often be of no trouble (because most things are still stable between versions), but for more advanced users, not having tracks would make the Snap package impossible to use, because advanced users need to control when they migrate to a new version (schedule the time necessary to update their files / projects).

4

Thanks for the detailed explanation. +1 for use of tracks, all the usual criteria are met by your description.

Let’s allow a few days for other @reviewers to vote and I’ll process this then. Thanks for your patience!

  • Daniel
1 Like
5

Is the “fast track creation” procedure gone? No problem reassessing our use of tracks, but we had them approved/created before.

6

It’s not gone! I checked and couldn’t find any tracks for coq-prover, it’s why I went for the full process - but it’s just because I was looking the wrong way. Thanks for reminding me. I’ve created the 2022.01 track now, cheers!

  • Daniel
1 Like