Merge branch 'master' into retract-locally-small

.github/workflows/ci.yaml

@@ -34,15 +34,15 @@ jobs:
         agda: ['2.7.0']
     steps:
       - name: Checkout our repository
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           path: master
       - name: Setup Agda
         uses: wenkokke/[email protected]
         with:
           agda-version: ${{ matrix.agda }}
 
-      - uses: actions/cache/restore@v3
+      - uses: actions/cache/restore@v4
         id: cache-agda-formalization
         name: Restore Agda formalization cache
         with:
@@ -61,13 +61,13 @@ jobs:
           make check
 
       - name: Save Agda build cache
-        uses: actions/cache/save@v3
+        uses: actions/cache/save@v4
         with:
           path: master/_build
           key: '${{ steps.cache-agda-formalization.outputs.cache-primary-key }}'
 
       # Install Python and friends for website generation only where needed
-      - uses: actions/setup-python@v4
+      - uses: actions/setup-python@v5
         if: ${{ matrix.os == 'ubuntu-latest' }}
         with:
           python-version: '3.8'
@@ -92,7 +92,7 @@ jobs:
       # keep the same key for a branch and update it on pushes.
       - name: Save pre-website cache
         if: ${{ matrix.os == 'ubuntu-latest' }}
-        uses: actions/cache/save@v3
+        uses: actions/cache/save@v4
         with:
           key: pre-website-${{ github.run_id }}
           path: master/docs
@@ -106,29 +106,29 @@ jobs:
       actions: write
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
         with:
           path: master
 
-      - uses: peaceiris/actions-mdbook@v1
+      - uses: peaceiris/actions-mdbook@v2
         with:
           mdbook-version: '0.4.34'
 
-      - uses: baptiste0928/cargo-install@v2
+      - uses: baptiste0928/cargo-install@v3
         with:
           crate: mdbook-linkcheck
           version: '0.7.7'
 
       # Install Python and friends for website generation only where needed
-      - uses: actions/setup-python@v4
+      - uses: actions/setup-python@v5
         with:
           python-version: '3.8'
           check-latest: true
           cache: 'pip'
 
       - run: python3 -m pip install -r master/scripts/requirements.txt
 
-      - uses: actions/cache/restore@v3
+      - uses: actions/cache/restore@v4
         with:
           key: pre-website-${{ github.run_id }}
           path: master/docs
@@ -162,14 +162,14 @@ jobs:
   pre-commit:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
 
-      - uses: actions/setup-python@v4
+      - uses: actions/setup-python@v5
         with:
           python-version: '3.8'
           check-latest: true
           cache: 'pip'
 
       - run: python3 -m pip install -r scripts/requirements.txt
 
-      - uses: pre-commit/[email protected].0
+      - uses: pre-commit/[email protected].1

.github/workflows/clean-up.yaml

@@ -9,7 +9,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Check out code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Cleanup
         run: |

.github/workflows/pages.yaml

@@ -32,7 +32,7 @@ jobs:
       id-token: write # to verify the deployment originates from an appropriate source
     steps:
       - name: Checkout our repository
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           path: master
           # We need the entire history for contributor information
@@ -43,7 +43,7 @@ jobs:
         with:
           agda-version: ${{ matrix.agda }}
 
-      - uses: actions/cache/restore@v3
+      - uses: actions/cache/restore@v4
         id: cache-agda-formalization
         name: Restore Agda formalization cache
         with:
@@ -56,35 +56,35 @@ jobs:
 
       # Keep versions in sync with the Makefile
       - name: MDBook setup
-        uses: peaceiris/actions-mdbook@v1
+        uses: peaceiris/actions-mdbook@v2
         with:
           mdbook-version: '0.4.34'
 
       - name: Install mdbook-pagetoc
-        uses: baptiste0928/cargo-install@v2
+        uses: baptiste0928/cargo-install@v3
         with:
           crate: mdbook-pagetoc
           version: '0.1.7'
 
       - name: Install mdbook-katex
-        uses: baptiste0928/cargo-install@v2
+        uses: baptiste0928/cargo-install@v3
         with:
           crate: mdbook-katex
           version: '0.5.7'
 
       - name: Install mdbook-linkcheck
-        uses: baptiste0928/cargo-install@v2
+        uses: baptiste0928/cargo-install@v3
         with:
           crate: mdbook-linkcheck
           version: '0.7.7'
 
       - name: Install mdbook-catppuccin
-        uses: baptiste0928/cargo-install@v2
+        uses: baptiste0928/cargo-install@v3
         with:
           crate: mdbook-catppuccin
           version: '1.2.0'
 
-      - uses: actions/setup-python@v4
+      - uses: actions/setup-python@v5
         with:
           python-version: '3.8'
           check-latest: true
@@ -100,21 +100,21 @@ jobs:
           make website
 
       - name: Setup Pages
-        uses: actions/configure-pages@v3
+        uses: actions/configure-pages@v5
         if: >-
           github.ref == 'refs/heads/master' || github.event_name ==
           'workflow_dispatch'
 
       - name: Upload artifact
-        uses: actions/upload-pages-artifact@v1
+        uses: actions/upload-pages-artifact@v3
         if: >-
           github.ref == 'refs/heads/master' || github.event_name ==
           'workflow_dispatch'
         with:
           path: master/book/html
 
       - name: Deploy to GitHub Pages
-        uses: actions/deploy-pages@v1
+        uses: actions/deploy-pages@v4
         id: deployment
         if: >-
           github.ref == 'refs/heads/master' || github.event_name ==

.github/workflows/profiling.yaml

@@ -19,7 +19,7 @@ jobs:
 
     steps:
       - name: Checkout our repository
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           path: repo