chore: bump toolchain to v4.22.0

.github/workflows/build.yml

@@ -3,25 +3,27 @@ on:
 
 name: continuous integration
 
-jobs:
-  # Cancels previous runs of jobs in this file
-  cancel:
-    name: 'Cancel Previous Runs (CI)'
-    runs-on: ubuntu-latest
-    # timeout-minutes: 3
-    steps:
-      - uses: styfle/cancel-workflow-action@0.12.1
-        with:
-          all_but_latest: true
-          access_token: ${{ github.token }}
+concurrency:
+  # label each workflow run; only the latest with each label will run
+  # workflows on master get more expressive labels
+  group: ${{ github.workflow }}-${{ github.ref }}.
+    ${{ ( contains(fromJSON( '["refs/heads/master", "refs/heads/staging"]'), github.ref ) && github.run_id) || ''}}
+  # cancel any running workflow with the same label
+  cancel-in-progress: true
 
+jobs:
   build:
     name: Build
     runs-on: ubuntu-latest
     steps:
       - name: cleanup
+        shell: bash    # This *just* deletes old files, so is safe to run outside landrun.
         run: |
-          find . -name . -o -prune -exec rm -rf -- {} +
+          if ! find . -mindepth 1 -exec rm -rf -- {} +; then
+            echo "ERROR: Initial cleanup failed, waiting 5 seconds and retrying..."
+            sleep 5
+            find . -mindepth 1 -exec rm -rf -- {} +
+          fi
           # Delete all but the 5 most recent toolchains.
           # Make sure to delete both the `~/.elan/toolchains/X` directory and the `~/.elan/update-hashes/X` file.
           # Skip symbolic links (`-type d`), the current directory (`! -name .`), and `nightly` and `stable`.
@@ -33,13 +35,17 @@ jobs:
 
       # The Hoskinson runners may not have jq installed, so do that now.
       - name: 'Setup jq'
-        uses: dcarbone/install-jq-action@v1.0.1
+        uses: dcarbone/install-jq-action@f0e10f46ff84f4d32178b4b76e1ef180b16f82c3 # v3.1.1
 
+      # NOTE: if you copy this, consider using `leanprover/lean-action` instead.
+      # We install manually, to avoid running lean outside landrun.
       - name: install elan
+        shell: bash
         run: |
           set -o pipefail
-          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
-          ./elan-init -y --default-toolchain none
+          curl -o elan-init.sh -sSfL https://elan.lean-lang.org/elan-init.sh
+          chmod +x elan-init.sh
+          ./elan-init.sh -y --default-toolchain none
           echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
 
       - uses: actions/checkout@v4
@@ -78,15 +84,12 @@ jobs:
 
       - name: update {Mutable, Algorithm}.lean
         id: mk_all
+        continue-on-error: true # Allow workflow to continue, outcome checked later
+        # This runs `mk_all --check` from the `pr-branch` inside landrun
         run: |
-
-          if ! lake exe mk_all --check
-          then
-            echo "Not all lean files are in the import all files"
-            echo "mk_all=false" >> "${GITHUB_OUTPUT}"
-          else
-            echo "mk_all=true" >> "${GITHUB_OUTPUT}"
-          fi
+          cd pr-branch
+          echo "Running mk_all --check (from pr-branch)..."
+          lake exe mk_all --check
 
       - name: build algorithm
         id: build

.github/workflows/docs.yml

@@ -6,6 +6,7 @@ on:
       - master
   pull_request:
 
+# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
 permissions:
   contents: read
   pages: write
@@ -21,11 +22,7 @@ jobs:
           rm -rf $HOME/.elan
           rm -rf $HOME/.cache/mathlib
 
-      - name: Checkout repo
-        uses: actions/checkout@v4
-        with:
-          fetch-depth: 2
-          lfs: true
+      - uses: actions/checkout@v4
 
       - name: install elan
         run: |
@@ -45,7 +42,7 @@ jobs:
 
       - name: build doc-gen4
         run: |
-          lake build doc-gen4
+          env DISABLE_EQUATIONS=1 lake build doc-gen4
 
       - name: build import graph
         run: |

Algorithm/Algebra/BigOperators/DFinsupp'.lean

@@ -26,7 +26,7 @@ namespace DFinsupp'
 section ProdAndSum
 
 /-- `DFinsupp'.prod f g` is the product of `g i (f i)` over the support of `f`. -/
-@[to_additive "`DFinsupp'.sum f g` is the sum of `g i (f i)` over the support of `f`."]
+@[to_additive /-- `DFinsupp'.sum f g` is the sum of `g i (f i)` over the support of `f`. -/]
 def prod [∀ (i) (x : β i), Decidable (x ≠ d i)] [CommMonoid γ] (f : Π₀' i, [β i, d i])
     (g : ∀ i, β i → γ) : γ :=
   ∏ i ∈ f.support, g i (f i)

Algorithm/Data/Classes/ToMultiset.lean

@@ -15,7 +15,7 @@ export Membership.IsEmpty (isEmpty isEmpty_iff_forall_not_mem)
 
 lemma isEmpty_eq_false_iff_exists_mem [Membership α C] [Membership.IsEmpty C] {c : C} :
     isEmpty c = false ↔ ∃ a, a ∈ c := by
-  rw [← Bool.eq_false_eq_not_eq_true, not_iff_comm, isEmpty_iff_forall_not_mem]
+  rw [Bool.eq_false_iff, not_iff_comm, isEmpty_iff_forall_not_mem]
   push_neg
   rfl
 

lake-manifest.json

@@ -5,27 +5,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "ab0dca34de1a12caedcf3f94a10bc9ed303f67da",
+   "rev": "58b48e75bd19f785927e06912dea610e5e48f1fa",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0-rc4",
+   "inputRev": "v4.22.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "928758ac3743dc7f171fc66f450506723896f1c5",
+   "rev": "79e94a093aff4a60fb1b1f92d9681e407124c2ca",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0-rc4",
+   "inputRev": "v4.22.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/mhuisi/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c682c91d2d4dd59a7187e2ab977ac25bd1f87329",
+   "rev": "6667b921594697980586296511fab6a359e802d1",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "bb6eb5b25892aa968e9d35f6ef9ca5c6b896c16d",
+   "rev": "d3195374a885cf2b0bfa66063deb493686029f95",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -48,14 +48,14 @@
    "rev": "dbfe2b7630c5f7c5c1cf71e7747ffc0a30337f69",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "dbfe2b7630c5f7c5c1cf71e7747ffc0a30337f69",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/acmepjz/md4lean",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b16338c5c66f57ef5510d4334eb6fa4e2c6c8cd8",
+   "rev": "feac4e0c356b0928657bf3b54fa83ae952f53257",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,17 +65,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c37191eba2da78393070da8c4367689d8c4276e4",
+   "rev": "b100ad4c5d74a464f497aaa8e7c74d86bf39a56f",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.22.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120",
+   "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,50 +85,50 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4241928fd3ebae83a037a253e39d9b773e34c3b4",
+   "rev": "eb164a46de87078f27640ee71e6c3841defc2484",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.22.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "96c67159f161fb6bf6ce91a2587232034ac33d7e",
+   "rev": "1253a071e6939b0faf5c09d2b30b0bfc79dae407",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.67",
+   "inputRev": "v0.0.68",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0a136f764a5dfedc4498e93ad8e297cff57ba2fc",
+   "rev": "1256a18522728c2eeed6109b02dd2b8f207a2a3c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.22.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1ef3dac0f872ca6aaa7d02e015427e06dd0b6195",
+   "rev": "917bfa5064b812b7fbd7112d018ea0b4def25ab3",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.22.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e96b5eca4fcfe2e0e96a1511a6cd5747515aba82",
+   "rev": "240676e9568c254a69be94801889d4b13f3b249f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.22.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "algorithm",

lakefile.lean

@@ -2,8 +2,8 @@ import Lake
 
 open Lake DSL
 
-require "leanprover-community" / "mathlib" @ git "v4.22.0-rc4"
-require "leanprover" / "doc-gen4" @ git "v4.22.0-rc4"
+require "leanprover-community" / "mathlib" @ git "v4.22.0"
+require "leanprover" / "doc-gen4" @ git "v4.22.0"
 
 abbrev algorithmOnlyLinters : Array LeanOption := #[
   ⟨`linter.mathlibStandardSet, true⟩,

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.22.0-rc4
+leanprover/lean4:v4.22.0