diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml index de909506295b8..abb030a2126bd 100644 --- a/.github/workflows/bors.yml +++ b/.github/workflows/bors.yml @@ -161,6 +161,18 @@ jobs: lean --version lake --version + - name: build cache cache + run: | + lake build cache + + - name: prune ProofWidgets .lake + run: | + # The ProofWidgets release contains not just the `.js` (which we need to build) + # but also `.oleans`, which may be built with the wrong toolchain. + # This removes them. + rm -rf .lake/packages/proofwidgets/.lake/build/lib + rm -rf .lake/packages/proofwidgets/.lake/build/ir + - name: get cache run: | lake exe cache clean diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index facc3d356f508..1ff81328af0f5 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -168,6 +168,18 @@ jobs: lean --version lake --version + - name: build cache cache + run: | + lake build cache + + - name: prune ProofWidgets .lake + run: | + # The ProofWidgets release contains not just the `.js` (which we need to build) + # but also `.oleans`, which may be built with the wrong toolchain. + # This removes them. + rm -rf .lake/packages/proofwidgets/.lake/build/lib + rm -rf .lake/packages/proofwidgets/.lake/build/ir + - name: get cache run: | lake exe cache clean diff --git a/.github/workflows/build.yml.in b/.github/workflows/build.yml.in index cffd2c5b5cd46..b42f4ee04ece5 100644 --- a/.github/workflows/build.yml.in +++ b/.github/workflows/build.yml.in @@ -147,6 +147,18 @@ jobs: lean --version lake --version + - name: build cache cache + run: | + lake build cache + + - name: prune ProofWidgets .lake + run: | + # The ProofWidgets release contains not just the `.js` (which we need to build) + # but also `.oleans`, which may be built with the wrong toolchain. + # This removes them. + rm -rf .lake/packages/proofwidgets/.lake/build/lib + rm -rf .lake/packages/proofwidgets/.lake/build/ir + - name: get cache run: | lake exe cache clean diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml index 95b38877f245c..7c66ea4af844b 100644 --- a/.github/workflows/build_fork.yml +++ b/.github/workflows/build_fork.yml @@ -165,6 +165,18 @@ jobs: lean --version lake --version + - name: build cache cache + run: | + lake build cache + + - name: prune ProofWidgets .lake + run: | + # The ProofWidgets release contains not just the `.js` (which we need to build) + # but also `.oleans`, which may be built with the wrong toolchain. + # This removes them. + rm -rf .lake/packages/proofwidgets/.lake/build/lib + rm -rf .lake/packages/proofwidgets/.lake/build/ir + - name: get cache run: | lake exe cache clean diff --git a/Mathlib/GroupTheory/Perm/Basic.lean b/Mathlib/GroupTheory/Perm/Basic.lean index ef4b9df6aeab6..4ac3cb1bc9490 100644 --- a/Mathlib/GroupTheory/Perm/Basic.lean +++ b/Mathlib/GroupTheory/Perm/Basic.lean @@ -587,7 +587,7 @@ theorem mul_swap_eq_iff {i j : α} {σ : Perm α} : σ * swap i j = σ ↔ i = j theorem swap_mul_swap_mul_swap {x y z : α} (hxy : x ≠ y) (hxz : x ≠ z) : swap y z * swap x y * swap y z = swap z x := by - nth_rewrite 2 [← swap_inv] + nth_rewrite 3 [← swap_inv] rw [← swap_apply_apply, swap_apply_left, swap_apply_of_ne_of_ne hxy hxz, swap_comm] #align equiv.swap_mul_swap_mul_swap Equiv.swap_mul_swap_mul_swap diff --git a/Mathlib/RingTheory/Polynomial/Hermite/Basic.lean b/Mathlib/RingTheory/Polynomial/Hermite/Basic.lean index c383b83153fbc..d21b4b7548141 100644 --- a/Mathlib/RingTheory/Polynomial/Hermite/Basic.lean +++ b/Mathlib/RingTheory/Polynomial/Hermite/Basic.lean @@ -172,7 +172,7 @@ theorem coeff_hermite_explicit : simp only -- Factor out (-1)'s. rw [mul_comm (↑k + _ : ℤ), sub_eq_add_neg] - nth_rw 3 [neg_eq_neg_one_mul] + nth_rw 2 [neg_eq_neg_one_mul] simp only [mul_assoc, ← mul_add, pow_succ] congr 2 -- Factor out double factorials. diff --git a/Mathlib/Tactic/NormNum/Core.lean b/Mathlib/Tactic/NormNum/Core.lean index 6ebf7ed63e1d7..d3450da515eb2 100644 --- a/Mathlib/Tactic/NormNum/Core.lean +++ b/Mathlib/Tactic/NormNum/Core.lean @@ -69,7 +69,7 @@ initialize normNumExt : ScopedEnvExtension Entry (Entry × NormNumExt) NormNums -- we only need this to deduplicate entries in the DiscrTree have : BEq NormNumExt := ⟨fun _ _ ↦ false⟩ /- Insert `v : NormNumExt` into the tree `dt` on all key sequences given in `kss`. -/ - let insert kss v dt := kss.foldl (fun dt ks ↦ dt.insertCore ks v discrTreeConfig) dt + let insert kss v dt := kss.foldl (fun dt ks ↦ dt.insertCore ks v) dt registerScopedEnvExtension { mkInitial := pure {} ofOLeanEntry := fun _ e@(_, n) ↦ return (e, ← mkNormNumExt n) diff --git a/Mathlib/Tactic/Positivity/Core.lean b/Mathlib/Tactic/Positivity/Core.lean index 755eb8cbe93ee..6df2444342089 100644 --- a/Mathlib/Tactic/Positivity/Core.lean +++ b/Mathlib/Tactic/Positivity/Core.lean @@ -74,7 +74,7 @@ initialize positivityExt : PersistentEnvExtension Entry (Entry × PositivityExt) (List Entry × DiscrTree PositivityExt) ← -- we only need this to deduplicate entries in the DiscrTree have : BEq PositivityExt := ⟨fun _ _ => false⟩ - let insert kss v dt := kss.foldl (fun dt ks => dt.insertCore ks v discrTreeConfig) dt + let insert kss v dt := kss.foldl (fun dt ks => dt.insertCore ks v) dt registerPersistentEnvExtension { mkInitial := pure ([], {}) addImportedFn := fun s => do diff --git a/Mathlib/Tactic/Propose.lean b/Mathlib/Tactic/Propose.lean index b83a8a6427eaa..2cb771a2235c6 100644 --- a/Mathlib/Tactic/Propose.lean +++ b/Mathlib/Tactic/Propose.lean @@ -54,7 +54,7 @@ initialize proposeLemmas : DeclCache (DiscrTree Name) ← let mut lemmas := lemmas for m in mvars do let path ← DiscrTree.mkPath (← inferType m) discrTreeConfig - lemmas := lemmas.insertIfSpecific path name discrTreeConfig + lemmas := lemmas.insertIfSpecific path name pure lemmas /-- Shortcut for calling `solveByElim`. -/ diff --git a/Mathlib/Tactic/Relation/Trans.lean b/Mathlib/Tactic/Relation/Trans.lean index df0b91d4958f8..4d55b9cfab49b 100644 --- a/Mathlib/Tactic/Relation/Trans.lean +++ b/Mathlib/Tactic/Relation/Trans.lean @@ -28,7 +28,7 @@ def transExt.config : WhnfCoreConfig := {} initialize transExt : SimpleScopedEnvExtension (Name × Array DiscrTree.Key) (DiscrTree Name) ← registerSimpleScopedEnvExtension { - addEntry := fun dt (n, ks) ↦ dt.insertCore ks n transExt.config + addEntry := fun dt (n, ks) ↦ dt.insertCore ks n initial := {} } diff --git a/lake-manifest.json b/lake-manifest.json index cb26596280b37..09a5bcd61761f 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -19,22 +19,22 @@ "inputRev": "master", "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/aesop", + {"url": "https://github.com/nomeata/aesop", "type": "git", "subDir": null, - "rev": "69404390bdc1de946bf0a2e51b1a69f308e56d7a", + "rev": "99334faa22c0e9979e8c79b748f2eb56a4358d7e", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "joachim/lean-3123", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "rev": "bf61e90de075abfa27f638922e7aafafdce77c44", + "rev": "8dd18350791c85c0fc9adbd6254c94a81d260d35", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.24-pre2", + "inputRev": "v0.0.25", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", diff --git a/lakefile.lean b/lakefile.lean index 1fd431f6de28c..fee10b3e4d491 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -28,8 +28,8 @@ require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main" require std from git "https://github.com/leanprover/std4" @ "nightly-testing" 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.24-pre2" +require aesop from git "https://github.com/nomeata/aesop" @ "joachim/lean-3123" +require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4" @ "v0.0.25" require Cli from git "https://github.com/leanprover/lean4-cli" @ "main" /-!