Please create a tag for the upcoming release of Coq 8.14 about aac-tactics HOT 6 CLOSED

Yes, I have seen the issue in my PR for bignums 8.14. I didn't see the problem before.

I guess it is reasonable then to put all packages which require 8.14 (or have an 8.14 in their version name) into extra-dev until 8.14.0 is released and then we do one PR to move over all such packages to released

Updated packages which are compatible with a range of Coq versions (e.g. mathcomp) can of course go immediately into released. This applies only to packages which require Coq 8.14.

from aac-tactics.

I have now created the tag v8.14.0 (https://github.com/coq-community/aac-tactics/releases/tag/v8.14.0) which is known to be compatible with 8.14+rc1.

Here is the opam file: https://github.com/coq/opam-coq-archive/blob/93b645e8642f0b4461e376ebdb8ab9124a3e74d4/extra-dev/packages/coq-aac-tactics/coq-aac-tactics.8.14.0/opam

from aac-tactics.

@palmskog : thanks! I just wonder why the opam package is in extra-dev. If you don't plan to change it for 8.14.0 I don't see a good reason for not publishing it as a release package. See e.g. (https://github.com/coq/opam-coq-archive/blob/master/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.1.12.0/opam) which also already has a 8.14 compatible package in released.

from aac-tactics.

Putting the package in released without a corresponding released Coq version the regular OCaml opam repo requires a radical restructuring of how we have handled betas and release candidates so far in the Coq opam repo. I think this should have been discussed beforehand. Looking through CEP 52, I don't see any mention of this.

@gares can you clarify what your intention was here? I thought we were going to handle pre-release packages just the same as last time.

from aac-tactics.

I just saw that there is a new tag v8.14.1 - shall I use this tag for Coq Platform 2021.11?

from aac-tactics.

I found an answer in coq/opam#1853 ... so I will use v8.14.1 for Coq Platform 2021.11.

from aac-tactics.