search

math-comp / algebra-tactics

Ring, field, lra, nra, and psatz tactics for Mathematical Components
33 stars 2 forks source link

Please pick the version you prefer for Coq 8.17 in Coq Platform 2023.03 #80

Closed MSoegtropIMC closed 1 year ago

MSoegtropIMC commented 1 year ago

The Coq team released Coq 8.17+rc1 on December 29th, 2022 and plans to release Coq 8.17.0 around March 7th, 2023. The corresponding Coq Platform release 2023.03 should be released before April 14th, 2023. It can be delayed in case of difficulties until June 30, 2023, 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.17+rc1.

Coq Platform CI is currently testing opam package coq-mathcomp-algebra-tactics.1.0.0 from platform patch repository https://github.com/coq/platform/tree/main/opam/opam-coq-archive/released/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.1.0.0/opam. This means we had to weaken some version restrictions in the opam package, 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 - please just close this issue.

In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2023.03, please inform us as soon as possible and before March 21st, 2023!

The working branch of Coq Platform, can be found here main. It contains package pick ~8.17~2023.03+preview1 which already supports Coq version 8.17+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/335

pi8027 commented 1 year ago

@MSoegtropIMC In fact, Algebra Tactics do not work with Coq 8.17 because of LPCIC/coq-elpi#436. It seems that we have to fix the issue in Coq-Elpi or Coq.

pi8027 commented 1 year ago

The issue in Coq-Elpi has been fixed in LPCIC/coq-elpi#438. The version constraints in the opam file will be fixed in coq/opam-coq-archive#2499.

MSoegtropIMC commented 1 year ago

Thanks! I checked that the updated opam package (with updated elpi) works fine and close this issue.

Just to double check: Coq Platform 2023.03 will use coq-mathcomp-algebra-tactics.1.0.0 - if this is not what you want, please reopen.

pi8027 commented 1 year ago

I changed my mind and decided to release coq-mathcomp-algebra-tactics.1.1.0. Please use this new version. https://github.com/math-comp/algebra-tactics/releases/tag/1.1.0

MSoegtropIMC commented 1 year ago

Thanks! I update coq-mathcomp-algebra-tactics in Coq Platform to version 1.1.0 and close this issue.

pi8027 commented 1 year ago

@MSoegtropIMC Would you mind updating the version of Algebra Tactics for the next Coq Platform release to 1.1.1? It fixes a minor issue.

MSoegtropIMC commented 1 year ago

Sure, no issue. The release is not done yet.

MSoegtropIMC commented 1 year ago

Thanks! I updated coq-mathcomp-algebra-tactics to version 1.1.1 in the 8.17 pick of Coq Platform 2023.03 and close this issue.