The Rocq team released Rocq 9.0.0 on March 12th, 2025.
The corresponding Rocq Platform release 2025.09 should be released before Oct 24th, 2025.
It can be delayed in case of difficulties until Nov 21st, 2025, but this should be an exception.

This issue is to inform you that the opam package we are currently testing in Rocq Platform CI works fine with Rocq 9.0.0.

Rocq Platform CI is currently testing opam package coq-unicoq.1.6+8.20
from platform patch repository https://github.com/rocq-prover/platform/tree/main/opam/opam-coq-archive/released/packages/coq-unicoq/coq-unicoq.1.6+8.20/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 Rocq 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 Rocq Platform 2025.09, please inform us as soon as possible and before Sep 26th, 2025!

The working branch of Rocq Platform, can be found here main.
It contains package pick ~9.0+preview~2025.08 which already supports Rocq version 9.0.0 and contains already working (possibly patched / commit pinned) Rocq 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 Rocq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Rocq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: rocq-prover/platform#481