update documentation and bump itauto to 9.1

doc/README_Linux.md

@@ -12,15 +12,15 @@ This method is intended for experienced users, who may want to use opam to insta
   - OpenSuse: `sudo zypper in -t pattern devel_C_C++`
 - For CentOS and possibly RHEL some additional steps are required, see [CentOS](#centos) below.
 - Get the Rocq Platform scripts via either of these methods
-  - Most users should download and extract `https://github.com/coq/platform/archive/refs/tags/2025.08.3.zip`.
-  - Users which intend to contribute to Rocq Platform should use `git clone --branch 2025.08.3 https://github.com/rocq-prover/platform.git`.
+  - Most users should download and extract `https://github.com/coq/platform/archive/refs/tags/2026.07.0.zip`.
+  - Users which intend to contribute to Rocq Platform should use `git clone --branch 2026.07.0 https://github.com/rocq-prover/platform.git`.
 - Open a shell, navigate to the download folder and execute `coq_platform_make.sh`.
 - The system will ask for sudo permissions to install prerequisites _several times_ so the script is not fully unattended but all installations of dependencies are done directly after the initialization of the opam switch.
 - In case the script aborts e.g. cause of internet issues, just rerun the script.
-- The script creates a new opam switch named e.g. CP.2025.08.0~9.0~2025.08 - the exact name depends on the Rocq version and package pick you selected.
+- The script creates a new opam switch named e.g. RP.2026.07.0~9.1~2026.01 - the exact name depends on the Rocq version and package pick you selected.
   This means the script does not touch your existing opam setup unless you already have a switch of this name.
 - Use the following commands to activate this switch after opening a new shell:
-  - `opam switch CP.2025.08.3~9.0~2025.08` (note: the switch name might vary if you choose a different version of Rocq - please use `opam switch` to see a list of switch names)
+  - `opam switch RP.2026.07.0~9.1~2026.01` (note: the switch name might vary if you choose a different version of Rocq - please use `opam switch` to see a list of switch names)
   - `eval $(opam env)`
   - The second step can be automated by rerunning `opam init`
 - The main opam repositories for Rocq and OCaml developments are already added to the created opam switch, so it should be easy to install additional Rocq (or OCaml) packages.

doc/README_Windows.md

@@ -23,8 +23,8 @@ This method is intended for experienced users, who may want to use opam to insta
 
 - In case you install **Rocq Platform for the first time**:
   - Get the Rocq Platform scripts via either of these methods
-    - Most users should download and extract `https://github.com/coq/platform/archive/refs/tags/2025.08.3.zip`.
-    - Users which intend to contribute to Coq Platform should use `git clone --branch 2025.08.3 https://github.com/rocq-prover/platform.git`.
+    - Most users should download and extract `https://github.com/coq/platform/archive/refs/tags/2026.07.0.zip`.
+    - Users which intend to contribute to Coq Platform should use `git clone --branch 2026.07.0 https://github.com/rocq-prover/platform.git`.
       Please note that the scripts are CR/LF sensitive, so if you use a Windows git client (not a Cygwin git) you should set `git config --global core.autocrlf false` - which is anyway a good idea.
   - Open a DOS command window, navigate to the download folder and execute `coq_platform_make_windows.bat`.
   - This will ask for the Cygwin installation path and setup a fresh Cygwin as build host (the created Rocq is MinGW and runs without Cygwin).
@@ -35,26 +35,26 @@ This method is intended for experienced users, who may want to use opam to insta
   - Start a cygwin shell via `C:\<your_coq_platform_Cygwin_path>\Cygwin.bat`
   - Download, clone or pull the Rocq Platform:
     - Download zip and expand:
-      - `wget https://github.com/coq/platform/archive/refs/tags/2025.08.3.zip`
-      - `unzip 2025.08.3.zip`
-      - `mv 2025.08.3 platform-2025.08.3``
-      - `cd platform-2025.08.3`
+      - `wget https://github.com/coq/platform/archive/refs/tags/2026.07.0.zip`
+      - `unzip 2026.07.0.zip`
+      - `mv 2025.08.3 platform-2026.07.0``
+      - `cd platform-2026.07.0`
     - **OR** Git clone:
-      - `git clone --branch 2025.08.3 https://github.com/rocq-prover/platform.git`
+      - `git clone --branch 2026.07.0 https://github.com/rocq-prover/platform.git`
       - `cd platform`
     - **OR** Git update (with existing git Coq Platform repo):
       - `cd platform`
-      - `git fetch & git checkout 2025.08.3`
+      - `git fetch & git checkout 2026.07.0`
   - Run the main Rocq Platform installation script `coq_platform_make.sh`
 - The script will ask a few questions if no parameters are given and then run fully unattended.
 - The build time is between 1..5 hours, depending on CPU speed and RAM size.
 - In case the script aborts e.g. cause of internet issues, just rerun the batch file - it won't install Cygwin again (assuming you specify the same Cygwin destination folder).
 - The script has various options for configuring paths and proxies; see `example_coq_platform_make.bat` for an example command line.
 - The resulting Rocq installation is opam based and best used from the Cygwin prompt (started via `C:\<your_coq_platform_Cygwin_path>\Cygwin.bat`)
-- The script creates a new opam switch named e.g. CP.2025.08.3~8.20~2025.01 - the exact name depends on the Rocq version and package pick you selected you selected.
+- The script creates a new opam switch named e.g. RP.2026.07.0~9.1~2026.01 - the exact name depends on the Rocq version and package pick you selected you selected.
   This means the script does not touch your existing opam setup unless you already have a switch of this name.
 - Use the following commands at the Cygwin prompt to activate this switch after opening a new shell:
-  - `opam switch CP.2025.08.3~9.0~2025.01` (note: the switch name might vary if you choose a different version of Rocq - please use `opam switch` to see a list of switch names)
+  - `opam switch RP.2026.07.0~9.1~2026.01` (note: the switch name might vary if you choose a different version of Rocq - please use `opam switch` to see a list of switch names)
   - `eval $(opam env)`
   - The second step can be automated by rerunning `opam init`
 - The main opam repositories for Rocq and OCaml developments are already added to the created opam switch, so it should be easy to install additional Rocq (or OCaml) packages.

doc/README_macOS.md

@@ -13,13 +13,13 @@ In case you want to use the fast path:
 
 - Download the DMG package from https://github.com/rocq-prover/platform/releases (click on "Assets" at the end of a release section).
 - Open the downloaded DMG package with a double click.
-- Drag and drop the "Rocq-Platform~9.0~2025.08.app" icon on the link to the "Applications" folder.
+- Drag and drop the "Rocq-Platform~9.1~2026.07.app" icon on the link to the "Applications" folder.
 - RocqIDE appears under `/Applications` in Finder and in Launcher.
 - The published installers are always signed by INRIA, but no notarized by Apple yet. This means that on first start of the application, you must right click on the Rocq application in the `Applications` folder and select `open`. Subsequently this is not required - the application can be started directly.
 - In case you want to use the installed `coqc` and other tools from the command line, you have three options:
   - Use the supplied `rocq-shell.command` file. This file is included in the top level folder of the `.dmg` file and can be dragged e.g. to the desktop and started from there. It opens a terminal window in which the environment variables `$PATH` and `$COQLIB` are set. These `.command` files always refer to a specifc version of Rocq, so you can keep multiple of these files for multiple versions of Rocq.
-  - Run `eval $(/Applications/Rocq-Platform~9.0~2025.08.app/Contents/Resources/bin/coq-env.sh)` in your shell. This will set the same environment variables as `rocq-shell.command` in the current shell.
-  - Add the folder `/Applications/Rocq-Platform~9.0~2025.08.app/Contents/Resources/bin` to your `$PATH`, e.g. by running `sudo sh -c "echo '/Applications/Rocq-Platform~9.0~2025.08.app/Contents/Resources/bin' > /etc/paths.d/coq"`. Please note that this method has two disadvantages: first it is difficult to switch between different versions of Rocq and second some tools require additional environment variables, e.g. `COQLIB` or `LD_LIBRARY_PATH` to be set.
+  - Run `eval $(/Applications/Rocq-Platform~9.1~2026.07.app/Contents/Resources/bin/coq-env.sh)` in your shell. This will set the same environment variables as `rocq-shell.command` in the current shell.
+  - Add the folder `/Applications/Rocq-Platform~9.1~2026.07.app/Contents/Resources/bin` to your `$PATH`, e.g. by running `sudo sh -c "echo '/Applications/Rocq-Platform~9.1~2026.07.app/Contents/Resources/bin' > /etc/paths.d/coq"`. Please note that this method has two disadvantages: first it is difficult to switch between different versions of Rocq and second some tools require additional environment variables, e.g. `COQLIB` or `LD_LIBRARY_PATH` to be set.
 - If you want to inspect the installed content, right click the `Rocq_Platform` app in `/Applications` in Finder and select `Show Package Contents`.
 
 **A note to lecturers:** it is easy to create a customized Windows installer from an opam switch - see [Customized Installers](FAQ-customized-installers.md)
@@ -37,15 +37,15 @@ This method is intended for experienced users, who may want to use opam to insta
 - If you have neither Homebrew nor MacPorts installed, read the section [Homebrew and MacPorts](#homebrew-and-macports) below.
 - If you have Homebrew installed, read the section [Homebrew issues and workarounds](#homebrew-issues-and-workarounds) below.
 - Get the Rocq Platform scripts via either of these methods
-  - Most users should download and extract `https://github.com/coq/platform/archive/refs/tags/2025.08.3.zip`.
-  - Users which intend to contribute to Rocq Platform should use `git clone --branch 2025.08.3 https://github.com/rocq-prover/platform.git`.
+  - Most users should download and extract `https://github.com/coq/platform/archive/refs/tags/2026.07.0.zip`.
+  - Users which intend to contribute to Rocq Platform should use `git clone --branch 2026.07.0 https://github.com/rocq-prover/platform.git`.
 - Open a shell, navigate to the download folder and execute `coq_platform_make.sh`.
 - If you are using MacPorts, the system will ask once for sudo permissions to install prerequisites after installing OCaml (5..20 minutes after script start).
 - In case the script aborts e.g. cause of internet issues, just rerun the script.
-- The script creates a new opam switch named e.g. CP.2025.01.0~8.20~2025.01 - the exact name depends on the Rocq version and package pick you selected.
+- The script creates a new opam switch named e.g. RP.2026.07.0~9.1~2026.01 - the exact name depends on the Rocq version and package pick you selected.
   This means the script does not touch your existing opam setup unless you already have a switch of this name.
 - Use the following commands to activate this switch after opening a new shell:
-  - `opam switch CP.2025.08.3~9.0~2025.01` (note: the switch name might vary if you choose a different version of Rocq - please use `opam switch` to see a list of switch names)
+  - `opam switch RP.2026.07.0~9.1~2026.01` (note: the switch name might vary if you choose a different version of Rocq - please use `opam switch` to see a list of switch names)
   - `eval $(opam env)`
   - The second step can be automated by rerunning `opam init`
 - The main opam repositories for Rocq and OCaml developments are already added to the created opam switch, so it should be easy to install additional Coq (or OCaml) packages.

doc/README~9.1~2026.01.md

@@ -1,5 +1,4 @@
-
-# Coq Platform 2026.02.0 providing Rocq 9.1 (released January 2026) with the preview package pick from Mars 2026
+# Coq Platform 2026.07.0 providing Rocq 9.1 (released January 2026) with the preview package pick from Mars 2026
 
 The [Coq proof assistant](https://coq.inria.fr) provides a formal language
 to write mathematical definitions, executable algorithms, and theorems, together
@@ -9,7 +8,7 @@ The [Coq Platform](https://github.com/coq/platform) is a distribution of the Coq
 interactive prover together with a selection of Coq libraries and plugins.
 
 The Coq Platform supports to install several versions of Coq (also in parallel).
-This README file is for **Coq Platform 2026.02.0 with Coq 9.1+rc1**.
+This README file is for **Coq Platform 2026.07.0 with Coq 9.1+rc1**.
 The README files for other versions are linked in the main [README](https://github.com/coq/platform/blob/main/README.md).
 
 This version of Rocq Platform 2026.01 includes Rocq 9.1 from January 2026.This is a **preview release** of the Rocq Platform for packages maintainers
@@ -22,8 +21,6 @@ The sections below provide a short description of each level and the list of
 packages included in each level. Packaged versions of the Coq Platform usually
 contain the **extended** set with all optional packages.
 
-
-
 **Note on non-free licenses:** The Coq Platform contains software with
 **non-free licenses which do not allow commercial use without purchasing a license**,
 notably the **coq-compcert** package. Please study the package licenses given
@@ -34,7 +31,7 @@ plan to use these packages.
 The license information given below is obtained from opam.
 The Coq Platform team does no double check this information.
 
-**Note on multiple licenses:** 
+**Note on multiple licenses:**
 In case several licenses are given below, it is not clearly specified what this means.
 It could mean that parts of the software use one license while other parts use another license.
 It could also mean that you can choose between the given licenses.
@@ -46,7 +43,7 @@ Please clarify the details with the homepage of the package.
 
 <br>
 
-## **Coq Platform 2026.02.0 with Coq 9.1+rc1 "base level"**
+## **Coq Platform 2026.07.0 with Coq 9.1+rc1 "base level"**
 
 The **base level** is mostly intended as a basis for custom installations using
 opam and contains the following package(s):
@@ -113,7 +110,7 @@ opam and contains the following package(s):
 
 <br>
 
-## **Coq Platform 2026.02.0 with Coq 9.1+rc1 "IDE level"**
+## **Coq Platform 2026.07.0 with Coq 9.1+rc1 "IDE level"**
 
 The **IDE level** adds an interactive development environment to the **base level**.
 
@@ -156,7 +153,7 @@ The **IDE level** contains the following package(s):
 
 <br>
 
-## **Coq Platform 2026.02.0 with Coq 9.1+rc1 "full level"**
+## **Coq Platform 2026.07.0 with Coq 9.1+rc1 "full level"**
 
 The **full level** adds many commonly used coq libraries, plug-ins and
 developments.
@@ -934,7 +931,7 @@ The **full level** contains the following packages:
 
 <br>
 
-## **Coq Platform 2026.02.0 with Coq 9.1+rc1 "optional packages"**
+## **Coq Platform 2026.07.0 with Coq 9.1+rc1 "optional packages"**
 
 The **optional** packages have the same maturity and maintenance level as the
 packages in the full level, but either take a rather long time to build or have
@@ -994,7 +991,7 @@ The following packages are **optional**:
 
 <br>
 
-## **Coq Platform 2026.02.0 with Coq 9.1+rc1 "extended level"**
+## **Coq Platform 2026.07.0 with Coq 9.1+rc1 "extended level"**
 
 The **extended level** contains packages which are in a beta stage or otherwise
 don't yet have the level of maturity or support required for inclusion in the
@@ -1687,4 +1684,3 @@ Please refer to the linked opam package and/or your system package manager for d
     <dt><b>description</b></dt><dd></dd>
   </dl>
 </details>
-

package_picks/coq_platform_release.sh

@@ -10,4 +10,4 @@
 
 ###################### SET THE PLATFORM VERSION NAME #####################
 
-COQ_PLATFORM_RELEASE="2026.02.0"
+COQ_PLATFORM_RELEASE="2026.07.0"

package_picks/package-pick-9.1~2026.01.sh

@@ -147,7 +147,7 @@ then
 
   PACKAGES="${PACKAGES} coq-coqeal.2.1.1" # modified
   PACKAGES="${PACKAGES} rocq-libhyps.4.0"
-  #PACKAGES="${PACKAGES} coq-itauto.8.20.0" # error
+  PACKAGES="${PACKAGES} coq-itauto.9.1.0"
 
   # General mathematics (which requires one of the above tools)
   PACKAGES="${PACKAGES} coq-mathcomp-analysis.1.16.0" # modified