chore: bump toolchain to v4.6.0 (#11065)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Feb 29, 2024 · 7ca43cb · 7ca43cb
1 parent 13e1315
commit 7ca43cb
Show file tree

Hide file tree

Showing 8 changed files with 14 additions and 15 deletions.
diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
@@ -296,7 +296,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          git checkout toolchain/v4.6.0-rc1
+          git checkout toolchain/v4.6.0
           # Now that the git hash is embedded in each olean,
           # we need to compile lean4checker on the same toolchain
           cp ../lean-toolchain .

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -303,7 +303,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          git checkout toolchain/v4.6.0-rc1
+          git checkout toolchain/v4.6.0
           # Now that the git hash is embedded in each olean,
           # we need to compile lean4checker on the same toolchain
           cp ../lean-toolchain .

diff --git a/.github/workflows/build.yml.in b/.github/workflows/build.yml.in
@@ -282,7 +282,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          git checkout toolchain/v4.6.0-rc1
+          git checkout toolchain/v4.6.0
           # Now that the git hash is embedded in each olean,
           # we need to compile lean4checker on the same toolchain
           cp ../lean-toolchain .

diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml
@@ -300,7 +300,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          git checkout toolchain/v4.6.0-rc1
+          git checkout toolchain/v4.6.0
           # Now that the git hash is embedded in each olean,
           # we need to compile lean4checker on the same toolchain
           cp ../lean-toolchain .

diff --git a/Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean b/Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean
@@ -308,7 +308,6 @@ theorem coeff_eq_zero : p.coeff n = 0 ↔ p n = 0 := by
   rw [← mkPiRing_coeff_eq p, ContinuousMultilinearMap.mkPiRing_eq_zero_iff]
 #align formal_multilinear_series.coeff_eq_zero FormalMultilinearSeries.coeff_eq_zero
 
-@[simp]
 theorem apply_eq_pow_smul_coeff : (p n fun _ => z) = z ^ n • p.coeff n := by simp
 #align formal_multilinear_series.apply_eq_pow_smul_coeff FormalMultilinearSeries.apply_eq_pow_smul_coeff
 

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -4,10 +4,10 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "cbc437aed076ea3aeb83f318d572f8b6de38265d",
+   "rev": "a7543d1a6934d52086971f510e482d743fe30cf3",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.6.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/quote4",
@@ -22,19 +22,19 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "82ac8cce559c3da0ade17cee3e275111fb7f1920",
+   "rev": "c51fa8ea4de8b203f64929cba19d139e555f9f6b",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.6.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "f5b2b6ff817890d85ffd8ed47637e36fcac544a6",
+   "rev": "16cae05860b208925f54e5581ec5fd264823440c",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.28",
+   "inputRev": "v0.0.29",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",

diff --git a/lakefile.lean b/lakefile.lean
@@ -26,10 +26,10 @@ package mathlib where
 meta if get_config? doc = some "on" then -- do not download and build doc-gen4 by default
 require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
 
-require std from git "https://github.com/leanprover/std4" @ "main"
+require std from git "https://github.com/leanprover/std4" @ "v4.6.0"
 require Qq from git "https://github.com/leanprover-community/quote4" @ "master"
-require aesop from git "https://github.com/leanprover-community/aesop" @ "master"
-require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4" @ "v0.0.28"
+require aesop from git "https://github.com/leanprover-community/aesop" @ "v4.6.0"
+require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4" @ "v0.0.29"
 require Cli from git "https://github.com/leanprover/lean4-cli" @ "main"
 require importGraph from git "https://github.com/leanprover-community/import-graph.git" @ "main"
 

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.6.0-rc1
+leanprover/lean4:v4.6.0