Merge pull request #245 from MSoegtropIMC/prepare-2022.03-9

Prepare 2022.03 9

.github/workflows/macos.yml

@@ -48,8 +48,8 @@ jobs:
       fail-fast: false
       matrix:
         variant:
-          - '8.15~2022.03'
-          - '8.14~2022.01'
+          - '8.15~2022.04'
+          - '8.14~2022.04'
 
     steps:
       - name: Git checkout
@@ -123,8 +123,8 @@ jobs:
       fail-fast: false
       matrix:
         variant:
-          - '8.15~2022.03'
-          - '8.14~2022.01'
+          - '8.15~2022.04'
+          - '8.14~2022.04'
 
     steps:
       - name: Install bash

.github/workflows/ubuntu.yml

@@ -28,7 +28,7 @@ on:
         default: '-extent=f -parallel=p -jobs=2 -vst=y -compcert=y -set-switch=y'
       snap_pick:
         description: 'Package pick for the snap package:'
-        default: 8.15~2022.03
+        default: 8.15~2022.04
       upload:
         description: 'Upload artifact to Snap Store? (true/false, default false)'
         default: false
@@ -39,7 +39,7 @@ on:
 env:
   PLATFORM: -extent=f -parallel=p -jobs=2 -vst=y -compcert=y -set-switch=y
   COQREGTESTING: y
-  SNAP_PICK: 8.15~2022.03
+  SNAP_PICK: 8.15~2022.04
 
 ###############################################################################
 # Ubuntu
@@ -57,8 +57,8 @@ jobs:
       matrix:
         variant:
           # This should contain all picks introduced in the current release + all original picks of all Coq versions
-          - '8.15~2022.03'
-          - '8.14~2022.03'
+          - '8.15~2022.04'
+          - '8.14~2022.04'
           - '8.14~2022.01'
           - '8.13~2021.02'
           - '8.12'

.github/workflows/windows.yml

@@ -54,8 +54,8 @@ jobs:
           - '64'
         variant:
           # Keep this in sync with the Smoke test below
-          - '8.15~2022.03'
-          - '8.14~2022.01'
+          - '8.15~2022.04'
+          - '8.14~2022.04'
 
     steps:
       - name: Set git to use LF
@@ -107,8 +107,8 @@ jobs:
           - '32'
           - '64'
         variant:
-          - '8.15~2022.03'
-          - '8.14~2022.01'
+          - '8.15~2022.04'
+          - '8.14~2022.04'
 
     steps:
       - name: 'Download Artifact'

README.md

@@ -34,8 +34,8 @@ The table below contains links to the README files for the supported versions
 of Coq and libraries. Each README file contains a list of included packages with
 detailed information for each package.
 
-- [Coq 8.15.0 (released Jan 2022) with the first package pick from Mar 2022](doc/README~8.15~2022.03.md)
-- [Coq 8.14.1 (released Nov 2021) with an updated package pick from Jan 2022](doc/README~8.14~2022.03.md)
+- [Coq 8.15.1 (released Mar 2022) with the first package pick from Apr 2022](doc/README~8.15~2022.04.md)
+- [Coq 8.14.1 (released Nov 2021) with an updated package pick from Apr 2022](doc/README~8.14~2022.04.md)
 - [Coq 8.14.1 (released Nov 2021) with the first package pick from Jan 2022](doc/README~8.14~2022.01.md)
 - [Coq 8.13.2 (released Apr 2021) with an updated package pick from Jan 2022](doc/README~8.13~2022.01.md)
 - [Coq 8.13.2 (released Apr 2021) with an updated package pick from Sep 2021](doc/README~8.13~2021.09.md)
@@ -70,31 +70,38 @@ The Coq Platform team does no double check this information.
 
 <details><summary><font size="+1">Release notes / changelog</font></summary>
 
-## Changes in 2022.03.0
+## Changes in 2022.04.0
 
-- release package pick for Coq 8.15.0 with many package version updates
-- re-enabled QuickChick on Windows
-- added `coq-ott` and `ott` to the "full" level (Ott is not available on Windows as yet)
+- release package pick for Coq 8.15.1 with many package version updates
+- a packahe pick for Coq 8.14.1, which is as much as possible compatible with the 8.15.1 pick
+- re-enabled QuickChick on Windows (please see notes below)
+- added `coq-ott` and `ott` to the "full" level
 - added `coq-relation-algebra` to the "full" level
 - added `coq-mathcomp-algebra-tactics` to the "extended" level
 - added `coq-extructures` to the "extended" level
 - many small usability improvements and fixes
 
-Please see the [Pick Readme](doc/README~8.15~2022.03.md) for details on new and updated packages.
+Please see the [Pick Readme](doc/README~8.15~2022.04.md) for details on new and updated packages.
 
 **Note on macOS**: CoqIDE was previously wrapped in a shell script to set the environment, which had the effect that
 it could not access the `documents` folder. This script has been replaced with a simple C program, so this should work now.
 
 **Note on `coq-flocq`**: there is a new version 4.0 for `coq-flocq` which is **not compatible** with the previous 3.X versions.
-Since some packages are not yet compatible with Flocq 4.0, notably `coq-compcert`, the 2022.03 picks contain both,
+Since some packages are not yet compatible with Flocq 4.0, notably `coq-compcert`, the 2022.04 picks contain both,
 `coq-flocq.4.0.0` and `coq-flocq.3.4.3`. Since one cannot install two version of one package, a new package called `coq-flocq3`
 has been added which uses `Flocq3` rather than `Flocq` as logical path. This way Flocq 3.X can be selected by using `Flocq3`
 in the `Require` commands and Flocq 4.X can be selected by using `Flocq` in the `Require` commands.
 The package `coq-compcert` has been patched to require `Flocq3`.
 For convenience the proof automation packages used for float proofs, `coq-gappa` and `coq-interval` are also available in
-a Flocq 3.X and Flocq 4.X variant. The Flocq 4.X variants have the usual named, the 3.X variants use the logical paths
+a Flocq 3.X and Flocq 4.X variant. The Flocq 4.X variants have the usual logical path, the 3.X variants use the logical paths
 `IntervalFlocq3` and `GappaFlocq3`.
 
+**Note on `coq-quickchick`**: QuickChick requires an OCaml compiler to run. The binary installers for Coq Platform do not
+provide OCaml, so QuickChick does not work with the binary installers for macOS, Windows and Snap.
+It is recommended to use the "compile from sources" method if you want to use QuickChick.
+An alternative method is to install OCaml by other means and have it in the PATH, but this method is not supported by the Coq Platform team.
+We plan to add an OCaml compiler to the binary installers in the next release.
+
 ## Changes in 2022.01.0
 
 - release package pick for Coq 8.14.0 + updated mostly compatible package pick for Coq 8.13.2
@@ -178,24 +185,24 @@ You can list the available switches with:
 ```
 ~$ opam switch
 #   switch                                 compiler                                              description
-    __coq-platform.2022.03.0~8.12          ocaml-base-compiler.4.10.2                            Coq 8.12.2 (released Dec 2020) with the first package pick from Dec 2020
-    __coq-platform.2022.03.0~8.13~2021.02  ocaml-base-compiler.4.10.2                            Coq 8.13.2 (released Apr 2021) with the first package pick from Feb 2021
-    __coq-platform.2022.03.0~8.13~2021.09  ocaml-base-compiler.4.10.2                            Coq 8.13.2 (released Apr 2021) with an extended package pick from Sep 2021
-    __coq-platform.2022.03.0~8.13~2022.01  ocaml-base-compiler.4.10.2                            Coq 8.13.2 (released Apr 2021) with an updated package pick from Jan 2022
-    __coq-platform.2022.03.0~8.14~2022.01  ocaml-option-flambda.1,ocaml-variants.4.12.1+options  Coq 8.14.1 (released Nov 2021) with the first package pick from Jan 2022
-    __coq-platform.2022.03.0~8.14~2022.03  ocaml-option-flambda.1,ocaml-variants.4.12.1+options  Coq 8.14.1 (released Nov 2021) with an updated package pick from Mar 2022
-    __coq-platform.2022.03.0~8.15~2022.03  ocaml-option-flambda.1,ocaml-variants.4.13.1+options  Coq 8.15.1 (released Mar 2022) with the first package pick from Mar 2022
-->  __coq-platform.2022.03.0~dev           ocaml-option-flambda.1,ocaml-variants.4.12.1+options  Coq dev (latest master of all packages)
+    __coq-platform.2022.04.0~8.12          ocaml-base-compiler.4.10.2                            Coq 8.12.2 (released Dec 2020) with the first package pick from Dec 2020
+    __coq-platform.2022.04.0~8.13~2021.02  ocaml-base-compiler.4.10.2                            Coq 8.13.2 (released Apr 2021) with the first package pick from Feb 2021
+    __coq-platform.2022.04.0~8.13~2021.09  ocaml-base-compiler.4.10.2                            Coq 8.13.2 (released Apr 2021) with an extended package pick from Sep 2021
+    __coq-platform.2022.04.0~8.13~2022.01  ocaml-base-compiler.4.10.2                            Coq 8.13.2 (released Apr 2021) with an updated package pick from Jan 2022
+    __coq-platform.2022.04.0~8.14~2022.01  ocaml-option-flambda.1,ocaml-variants.4.12.1+options  Coq 8.14.1 (released Nov 2021) with the first package pick from Jan 2022
+    __coq-platform.2022.04.0~8.14~2022.04  ocaml-option-flambda.1,ocaml-variants.4.12.1+options  Coq 8.14.1 (released Nov 2021) with an updated package pick from Apr 2022
+    __coq-platform.2022.04.0~8.15~2022.04  ocaml-option-flambda.1,ocaml-variants.4.13.1+options  Coq 8.15.1 (released Mar 2022) with the first package pick from Apr 2022
+->  __coq-platform.2022.04.0~dev           ocaml-option-flambda.1,ocaml-variants.4.12.1+options  Coq dev (latest master of all packages)
 ```
 
 You can select the opam switch for **all shells** with e.g.:
 ```
-~$ opam switch __coq-platform.2022.03.0~8.15~2022.03
+~$ opam switch __coq-platform.2022.04.0~8.15~2022.04
 ```
 
 You can select the opam switch for **just the current shell** with e.g.:
 ```
-eval $(opam config env --set-switch --switch __coq-platform.2022.03.0~8.15~2022.03)
+eval $(opam config env --set-switch --switch __coq-platform.2022.04.0~8.15~2022.04)
 ```
 
 So you can easily open two separate shell windows, select different opam switches and start e.g. two CoqIDE instances to step through the same file with two different versions of Coq.
@@ -234,18 +241,18 @@ Please clarify the license at [CompCert License](https://github.com/AbsInt/CompC
     ```
     ~$ opam switch
     #   switch                                 compiler                                              description
-        __coq-platform.2022.03.0~8.12          ocaml-base-compiler.4.10.2                            Coq 8.12.2 (released Dec 2020) with the first package pick from Dec 2020
-        __coq-platform.2022.03.0~8.13~2021.02  ocaml-base-compiler.4.10.2                            Coq 8.13.2 (released Apr 2021) with the first package pick from Feb 2021
-        __coq-platform.2022.03.0~8.13~2021.09  ocaml-base-compiler.4.10.2                            Coq 8.13.2 (released Apr 2021) with an extended package pick from Sep 2021
-        __coq-platform.2022.03.0~8.13~2022.01  ocaml-base-compiler.4.10.2                            Coq 8.13.2 (released Apr 2021) with an updated package pick from Jan 2022
-        __coq-platform.2022.03.0~8.14~2022.01  ocaml-option-flambda.1,ocaml-variants.4.12.1+options  Coq 8.14.1 (released Nov 2021) with the first package pick from Jan 2022
-        __coq-platform.2022.03.0~8.14~2022.03  ocaml-option-flambda.1,ocaml-variants.4.12.1+options  Coq 8.14.1 (released Nov 2021) with an updated package pick from Mar 2022
-        __coq-platform.2022.03.0~8.15~2022.03  ocaml-option-flambda.1,ocaml-variants.4.13.1+options  Coq 8.15.1 (released Mar 2022) with the first package pick from Mar 2022
-    ->  __coq-platform.2022.03.0~dev           ocaml-option-flambda.1,ocaml-variants.4.12.1+options  Coq dev (latest master of all packages)
+        __coq-platform.2022.04.0~8.12          ocaml-base-compiler.4.10.2                            Coq 8.12.2 (released Dec 2020) with the first package pick from Dec 2020
+        __coq-platform.2022.04.0~8.13~2021.02  ocaml-base-compiler.4.10.2                            Coq 8.13.2 (released Apr 2021) with the first package pick from Feb 2021
+        __coq-platform.2022.04.0~8.13~2021.09  ocaml-base-compiler.4.10.2                            Coq 8.13.2 (released Apr 2021) with an extended package pick from Sep 2021
+        __coq-platform.2022.04.0~8.13~2022.01  ocaml-base-compiler.4.10.2                            Coq 8.13.2 (released Apr 2021) with an updated package pick from Jan 2022
+        __coq-platform.2022.04.0~8.14~2022.01  ocaml-option-flambda.1,ocaml-variants.4.12.1+options  Coq 8.14.1 (released Nov 2021) with the first package pick from Jan 2022
+        __coq-platform.2022.04.0~8.14~2022.04  ocaml-option-flambda.1,ocaml-variants.4.12.1+options  Coq 8.14.1 (released Nov 2021) with an updated package pick from Apr 2022
+        __coq-platform.2022.04.0~8.15~2022.04  ocaml-option-flambda.1,ocaml-variants.4.13.1+options  Coq 8.15.1 (released Mar 2022) with the first package pick from Apr 2022
+    ->  __coq-platform.2022.04.0~dev           ocaml-option-flambda.1,ocaml-variants.4.12.1+options  Coq dev (latest master of all packages)
     ```
 - Choose the switch you want to change with this command (example):
     ```
-    opam switch __coq-platform.2022.03.0~8.15~2022.03
+    opam switch __coq-platform.2022.04.0~8.15~2022.04
     eval $(opam env)
     ```
 - You can find packages with `opam list --all | grep "some keyword"`.

doc/README~8.12.md

@@ -1,4 +1,4 @@
-# Coq Platform 2022.03.0 providing Coq 8.12.2 (released Dec 2020) with the first package pick from Dec 2020
+# Coq Platform 2022.04.0 providing Coq 8.12.2 (released Dec 2020) with the first package pick from Dec 2020
 
 The [Coq proof assistant](https://coq.inria.fr) provides a formal language
 to write mathematical definitions, executable algorithms, and theorems, together
@@ -8,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 2022.03.0 with Coq 8.12.2**.
+This README file is for **Coq Platform 2022.04.0 with Coq 8.12.2**.
 The README files for other versions are linked in the main [README](../README.md).
 
 This version of Coq Platform 2022.01.0 includes Coq 8.12.2 from 12/2020. The package pick is the original package pick of Coq Platform for Coq 8.12.2. 
@@ -41,7 +41,7 @@ Please clarify the details with the homepage of the package.
 
 <br>
 
-## **Coq Platform 2022.03.0 with Coq 8.12.2 "base level"**
+## **Coq Platform 2022.04.0 with Coq 8.12.2 "base level"**
 
 The **base level** is mostly intended as a basis for custom installations using
 opam and contains the following package(s):
@@ -63,7 +63,7 @@ opam and contains the following package(s):
 
 <br>
 
-## **Coq Platform 2022.03.0 with Coq 8.12.2 "IDE level"**
+## **Coq Platform 2022.04.0 with Coq 8.12.2 "IDE level"**
 
 The **IDE level** adds an interactive development environment to the **base level**.
 
@@ -91,7 +91,7 @@ The **IDE level** contains the following package(s):
 
 <br>
 
-## **Coq Platform 2022.03.0 with Coq 8.12.2 "full level"**
+## **Coq Platform 2022.04.0 with Coq 8.12.2 "full level"**
 
 The **full level** adds many commonly used coq libraries, plug-ins and
 developments.
@@ -494,7 +494,7 @@ The **full level** contains the following packages:
 
 <br>
 
-## **Coq Platform 2022.03.0 with Coq 8.12.2 "optional packages"**
+## **Coq Platform 2022.04.0 with Coq 8.12.2 "optional packages"**
 
 The **optional** packages have the same maturity and maintenance level as the
 packages in the full level, but either have a **non open source license** or
@@ -539,7 +539,7 @@ The following packages are **optional**:
 
 <br>
 
-## **Coq Platform 2022.03.0 with Coq 8.12.2 "extended level"**
+## **Coq Platform 2022.04.0 with Coq 8.12.2 "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

doc/README~8.13~2021.02.md

@@ -1,4 +1,4 @@
-# Coq Platform 2022.03.0 providing Coq 8.13.2 (released Apr 2021) with the first package pick from Feb 2021
+# Coq Platform 2022.04.0 providing Coq 8.13.2 (released Apr 2021) with the first package pick from Feb 2021
 
 The [Coq proof assistant](https://coq.inria.fr) provides a formal language
 to write mathematical definitions, executable algorithms, and theorems, together
@@ -8,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 2022.03.0 with Coq 8.13.2**.
+This README file is for **Coq Platform 2022.04.0 with Coq 8.13.2**.
 The README files for other versions are linked in the main [README](../README.md).
 
 This version of Coq Platform 2022.01.0 includes Coq 8.13.2 from 04/2021. There are three package picks for Coq 8.13.2: the original from 02/2021, a substantially extended one from 09/2021 and an updated one from 11/2021. This is the original package pick for Coq 8.13 from 02/2021. The 02/2021 and 09/2021 package picks are provided for compatibility and it is recommended to use the 11/2021 pick - or Coq 8.14.0.
@@ -41,7 +41,7 @@ Please clarify the details with the homepage of the package.
 
 <br>
 
-## **Coq Platform 2022.03.0 with Coq 8.13.2 "base level"**
+## **Coq Platform 2022.04.0 with Coq 8.13.2 "base level"**
 
 The **base level** is mostly intended as a basis for custom installations using
 opam and contains the following package(s):
@@ -63,7 +63,7 @@ opam and contains the following package(s):
 
 <br>
 
-## **Coq Platform 2022.03.0 with Coq 8.13.2 "IDE level"**
+## **Coq Platform 2022.04.0 with Coq 8.13.2 "IDE level"**
 
 The **IDE level** adds an interactive development environment to the **base level**.
 
@@ -91,7 +91,7 @@ The **IDE level** contains the following package(s):
 
 <br>
 
-## **Coq Platform 2022.03.0 with Coq 8.13.2 "full level"**
+## **Coq Platform 2022.04.0 with Coq 8.13.2 "full level"**
 
 The **full level** adds many commonly used coq libraries, plug-ins and
 developments.
@@ -509,7 +509,7 @@ The **full level** contains the following packages:
 
 <br>
 
-## **Coq Platform 2022.03.0 with Coq 8.13.2 "optional packages"**
+## **Coq Platform 2022.04.0 with Coq 8.13.2 "optional packages"**
 
 The **optional** packages have the same maturity and maintenance level as the
 packages in the full level, but either have a **non open source license** or
@@ -554,7 +554,7 @@ The following packages are **optional**:
 
 <br>
 
-## **Coq Platform 2022.03.0 with Coq 8.13.2 "extended level"**
+## **Coq Platform 2022.04.0 with Coq 8.13.2 "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