Merge branch 'master' into ps/branch/smallness

HoTT · Sep 21, 2024 · e839d96 · e839d96
2 parents 8a786e7 + 61fbd65
commit e839d96
Show file tree

Hide file tree

Showing 268 changed files with 20,715 additions and 7,144 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -8,7 +8,7 @@ concurrency:
 
 # We set the supported coq-version from here. In order to use this environment variable correctly, look at how they are used in the following jobs.
 env:
-  coq-version-supported: '8.18'
+  coq-version-supported: '8.19'
   ocaml-version: '4.14-flambda'
   deployment-branch: 'gh-pages'
 
@@ -36,7 +36,6 @@ jobs:
       matrix:
         coq-version-dummy:
         - 'supported'
-        - '8.18'
         - 'latest'
         - 'dev'
         os:
@@ -51,7 +50,7 @@ jobs:
       run: echo "coq-version=${{ env.coq-version-supported }}" >> $GITHUB_ENV
 
     - name: Checkout repo
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
     - name: Build HoTT
       uses: coq-community/docker-coq-action@v1
       with:
@@ -82,7 +81,7 @@ jobs:
       if: matrix.coq-version-dummy == 'supported'
       run: echo "coq-version=${{ env.coq-version-supported }}" >> $GITHUB_ENV
     - name: Checkout repo
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
     - name: Build HoTT
       uses: coq-community/docker-coq-action@v1
       with:
@@ -120,7 +119,7 @@ jobs:
       if: matrix.coq-version-dummy == 'supported'
       run: echo "coq-version=${{ env.coq-version-supported }}" >> $GITHUB_ENV
     # Checkout branch
-    - uses: actions/checkout@v3
+    - uses: actions/checkout@v4
       with:
         submodules: recursive
     # We use the coq docker so we don't have to build coq
@@ -134,7 +133,7 @@ jobs:
           endGroup
           echo "::remove-matcher owner=coq-problem-matcher::" # remove problem matcher installed by Coq docker action, so we don't get duplicate warning annotations
           sudo apt-get -o Acquire::Retries=30 update -q
-          sudo apt-get -o Acquire::Retries=30 install python -y --allow-unauthenticated
+          sudo apt-get -o Acquire::Retries=30 install python3 python-is-python3 -y --allow-unauthenticated
           etc/coq-scripts/github/reportify-coq.sh --errors ${{ matrix.extra-gh-reportify }} make TIMED=1 -j2 --output-sync
 
     - name: Revert permissions
@@ -146,7 +145,7 @@ jobs:
       run: tar -cf workspace.tar .
     # We upload build artifacts for use by documentation
     - name: 'Upload Artifact'
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: workspace-${{ env.coq-version }}
         path: workspace.tar
@@ -155,7 +154,7 @@ jobs:
   nix:
     runs-on: ubuntu-latest
     steps:
-    - uses: actions/checkout@v3
+    - uses: actions/checkout@v4
     - uses: cachix/install-nix-action@v20
       with:
         name: coq-hott
@@ -181,11 +180,11 @@ jobs:
     needs: build
     runs-on: ubuntu-latest
     steps:
-    - uses: actions/checkout@v3
+    - uses: actions/checkout@v4
       with:
         submodules: recursive
     # Download artifact
-    - uses: actions/download-artifact@v3
+    - uses: actions/download-artifact@v4
       with:
         name: workspace-${{ env.coq-version-supported }}
     # Unpack Tar
@@ -203,11 +202,16 @@ jobs:
         custom_script: |
           opam install -y coq-serapi
           sudo apt-get -o Acquire::Retries=30 update -q
-          sudo apt-get -o Acquire::Retries=30 install python3-pip autoconf -y --allow-unauthenticated
-          python3 -m pip install --user --upgrade pygments dominate beautifulsoup4 docutils==0.17.1
+          sudo apt-get -o Acquire::Retries=30 install python3-pip python3-venv autoconf -y --allow-unauthenticated
           startGroup "Workaround permission issue" # https://github.com/coq-community/docker-coq-action#permissions
             sudo chown -R coq:coq .
           endGroup
+          # Create and activate a virtual environment
+          python3 -m venv myenv
+          source myenv/bin/activate
+          # Install the required Python packages in the virtual environment
+          python -m pip install --upgrade pip
+          python -m pip install pygments dominate beautifulsoup4 docutils==0.17.1
           echo "::remove-matcher owner=coq-problem-matcher::" # remove problem matcher installed by Coq docker action, so we don't get duplicate warning annotations
           make alectryon ALECTRYON_EXTRAFLAGS=--traceback
     - name: Revert permissions
@@ -217,7 +221,7 @@ jobs:
     - name: tar alectryon artifact
       run: tar -cf alectryon-html.tar alectryon-html
     - name: upload alectryon artifact
-      uses: actions/upload-artifact@v1
+      uses: actions/upload-artifact@v4
       with:
         name: alectryon-html
         path: alectryon-html.tar
@@ -229,11 +233,11 @@ jobs:
     runs-on: ubuntu-latest
     steps:
     # Checkout branch
-    - uses: actions/checkout@v3
+    - uses: actions/checkout@v4
       with:
         submodules: recursive
     # Download artifact
-    - uses: actions/download-artifact@v3
+    - uses: actions/download-artifact@v4
       with:
         name: workspace-${{ env.coq-version-supported }}
     # Unpack Tar
@@ -273,7 +277,7 @@ jobs:
           mv HoTT.svg HoTTCore.svg dep-graphs/
 
           ## Install coq-dpdgraph
-          opam install coq-dpdgraph.1.0+8.18 -y
+          opam install coq-dpdgraph.1.0+8.19 -y
 
           # For some reason, we get a stackoverflow. So we are lax
           # with making these.
@@ -300,12 +304,12 @@ jobs:
         tar -cf file-dep-graphs.tar file-dep-graphs
     # We upload the artifacts
     - name: 'Upload Artifact dep-graphs.tar'
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: dep-graphs
         path: dep-graphs.tar
     - name: 'Upload Artifact file-dep-graphs.tar'
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: file-dep-graphs
         path: file-dep-graphs.tar
@@ -317,11 +321,11 @@ jobs:
     runs-on: ubuntu-latest
     steps:
     # Checkout branch
-    - uses: actions/checkout@v3
+    - uses: actions/checkout@v4
       with:
         submodules: recursive
     # Download artifact
-    - uses: actions/download-artifact@v3
+    - uses: actions/download-artifact@v4
       with:
         name: workspace-${{ env.coq-version-supported }}
     # Unpack Tar
@@ -348,7 +352,7 @@ jobs:
       run: tar -cf coqdoc-html.tar coqdoc-html
     # Upload coqdoc-html artifact
     - name: 'Upload coqdoc-html Artifact'
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: coqdoc-html
         path: coqdoc-html.tar
@@ -360,11 +364,11 @@ jobs:
     runs-on: ubuntu-latest
     steps:
     # Checkout branch
-    - uses: actions/checkout@v3
+    - uses: actions/checkout@v4
       with:
         submodules: recursive
     # Download artifact
-    - uses: actions/download-artifact@v3
+    - uses: actions/download-artifact@v4
       with:
         name: workspace-${{ env.coq-version-supported }}
     # Unpack Tar
@@ -376,7 +380,7 @@ jobs:
         ocaml_version: ${{ env.ocaml-version }}
         custom_script: |
           sudo apt-get update
-          sudo apt-get install -y time python lua5.1
+          sudo apt-get install -y time python3 python-is-python3 lua5.1
           startGroup "Workaround permission issue" # https://github.com/coq-community/docker-coq-action#permissions
             sudo chown -R coq:coq .
           endGroup
@@ -392,7 +396,7 @@ jobs:
       run: tar -cf timing-html.tar timing-html
     # Upload timing-html artifact
     - name: 'Upload timing-html Artifact'
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: timing-html
         path: timing-html.tar
@@ -417,11 +421,11 @@ jobs:
       if: matrix.coq-version-dummy == 'supported'
       run: echo "coq-version=${{ env.coq-version-supported }}" >> $GITHUB_ENV
     # Checkout branch
-    - uses: actions/checkout@v3
+    - uses: actions/checkout@v4
       with:
         submodules: recursive
     # Download artifact
-    - uses: actions/download-artifact@v3
+    - uses: actions/download-artifact@v4
       with:
         name: workspace-${{ env.coq-version }}
     # Unpack Tar
@@ -462,11 +466,11 @@ jobs:
       if: matrix.coq-version-dummy == 'supported'
       run: echo "coq-version=${{ env.coq-version-supported }}" >> $GITHUB_ENV
     # Checkout branch
-    - uses: actions/checkout@v3
+    - uses: actions/checkout@v4
       with:
         submodules: recursive
     # Download artifact
-    - uses: actions/download-artifact@v3
+    - uses: actions/download-artifact@v4
       with:
         name: workspace-${{ env.coq-version }}
     # Unpack Tar
@@ -508,25 +512,25 @@ jobs:
     runs-on: ubuntu-latest
     steps:
     # Checkout branch
-    - uses: actions/checkout@v3
+    - uses: actions/checkout@v4
     # Download alectryon artifact
-    - uses: actions/download-artifact@v3
+    - uses: actions/download-artifact@v4
       with:
         name: alectryon-html
     # Download dependency graph artifacts
-    - uses: actions/download-artifact@v3
+    - uses: actions/download-artifact@v4
       with:
         name: dep-graphs
     # Download file dependency graph artifacts
-    - uses: actions/download-artifact@v3
+    - uses: actions/download-artifact@v4
       with:
         name: file-dep-graphs
     # Download coqdoc artifact
-    - uses: actions/download-artifact@v3
+    - uses: actions/download-artifact@v4
       with:
         name: coqdoc-html
     # Download timing artifact
-    - uses: actions/download-artifact@v3
+    - uses: actions/download-artifact@v4
       with:
         name: timing-html
     # Unpack Tar files

diff --git a/.gitignore b/.gitignore
@@ -110,3 +110,6 @@ _CoqProject
 
 # ignore nix profiles
 nix/profiles/
+
+# Ignore the file to bench
+file_to_bench
diff --git a/INSTALL.md b/INSTALL.md
@@ -5,6 +5,9 @@ library to use in your own project or to play around with.
 
 - [1. Installation using Coq Platform](#1-installation-using-coq-platform)
 - [2. Installation of HoTT library using opam](#2-installation-of-hott-library-using-opam)
+  - [Released Versions](#released-versions)
+  - [Source Versions](#source-versions)
+  - [Development Versions](#development-versions)
 - [3. Setup for developers (using git)](#3-setup-for-developers-using-git)
   - [3.1. Prequisites (Installing Coq)](#31-prequisites-installing-coq)
     - [3.1.1. Development in OSX and Windows](#311-development-in-osx-and-windows)
@@ -50,8 +53,18 @@ wish to import the entire library you can write:
 From HoTT Require Import HoTT.
 ```
 
+> ### Warning
+>
+> The versions of the HoTT library appearing in the Coq Platform are released
+> twice a year. This means that there is a good chance that the Coq Platform
+> version is lagging behind the latest version of the library. If you wish to
+> use the latest version of the library, you should install it using `opam` as
+> described in the next section.
+
 # 2. Installation of HoTT library using opam
 
+## Released Versions
+
 More advanced users may wish to install the HoTT library via `opam` ([See here
 for details on installing `opam`][3]). You need to add the released coq-archive
 packages to `opam` which can be done as follows:
@@ -66,12 +79,24 @@ library is `coq-hott` inside the coq-archive.
 $ opam install coq-hott
 ```
 
+## Source Versions
+
+After cloning the repository, you can install the library using `opam` by running
+`opam install .` in the root of the repository.
+
+## Development Versions
+
 We also have the current development versions of the library available via
 `opam`. For this however, you will need to add the dev coq-archive packages:
 ```shell
+$ opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
 $ opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
 ```
 
+This will make `coq.dev` the latest available version of `coq`. You can pin
+`coq` to a stable version by running `opam pin add coq.dev 8.19.1` for example.
+Then install the library with `opam install coq-hott`, as for the released version.
+
 # 3. Setup for developers (using git)
 
 ## 3.1. Prequisites (Installing Coq)
@@ -162,7 +187,8 @@ We recommend the following text editors for the development of `.v` files:
 
  * [Emacs][10] together with [Proof General][11].
  * [CoqIDE][12] part of the [Coq Proof Assistant][13].
- * [Visual Studio Code][14] together with [VSCoq][15].
+ * [Visual Studio Code][14] together with [coq-lsp][15].
+ * For more editors, see the Coq website article on [User Interfaces][19].
 
 ## 4.1. Tags for Emacs
 
@@ -220,7 +246,9 @@ GitHub](https://github.com/HoTT/HoTT).
 [12]: https://coq.inria.fr/refman/practical-tools/coqide.html
 [13]: https://github.com/coq/coq
 [14]: https://code.visualstudio.com/
-[15]: https://github.com/coq-community/vscoq
+[15]: https://github.com/ejgallego/coq-lsp
+
 [16]: https://cygwin.com/install.html
 [17]: https://stackoverflow.com/a/54086635
 [18]: https://git-scm.com/book/en/v2/Getting-Started-Installing-Git
+[19]: https://coq.inria.fr/user-interfaces.html
diff --git a/README.md b/README.md
@@ -47,14 +47,9 @@ your `_CoqProject` file:
 
 For more advanced use such as contribution see [INSTALL.md](/INSTALL.md).
 
-We recommend the following text editors:
-
- * [Emacs][16] together with [Proof General][17].
- * [CoqIDE][18] part of the [Coq Proof Assistant][19].
- * [Visual Studio Code][20] together with [VSCoq][21].
-
-Other methods of developing in `coq` will work as long as the correct arguments
-are passed.
+For **recommended text editors** see [our recommended editors
+list](./INSTALL.md#4-editors). Other methods of developing in `coq` will work as
+long as the correct arguments are passed.
 
 # Contributing
 
@@ -92,11 +87,4 @@ More information can be found in the [Wiki][22].
 [14]: https://github.com/HoTT/HoTT/wiki/Publications-based-on-the-HoTT-library
 [15]: https://github.com/coq/platform/releases
 
-[16]: http://www.gnu.org/software/emacs/
-[17]: http://proofgeneral.inf.ed.ac.uk
-[18]: https://coq.inria.fr/refman/practical-tools/coqide.html
-[19]: https://github.com/coq/coq
-[20]: https://code.visualstudio.com/
-[21]: https://github.com/coq-community/vscoq
-
 [22]: https://github.com/HoTT/HoTT/wiki