Merge pull request #9438 from leanprover-community/joachim/nightly-te…

…sting-fix-01-03

chore: fix nightly testing to work with 2024-01-03

.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

.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

.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

.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

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
 

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.

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)

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

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`. -/

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 := {}
   }
 

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",

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"
 
 /-!