chore: adaptations for leanprover/lean4#3123 (#9453)

This is the adapation PR for leanprover/lean4#3123. It will be merged to `bump/v4.6.0` *after* `#9452. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Jan 7, 2024 · 5a0907e · 5a0907e
1 parent 2c20845
commit 5a0907e
Show file tree

Hide file tree

Showing 7 changed files with 11 additions and 11 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -4,10 +4,10 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "4f632e6fac86f6c3b7d4ac127c0ce8b06ab86f63",
+   "rev": "e8114d048e20888a200db19aae1aada664ecec8c",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "4f632e6fac86f6c3b7d4ac127c0ce8b06ab86f63",
+   "inputRev": "bump/v4.6.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/quote4",
@@ -22,10 +22,10 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "69404390bdc1de946bf0a2e51b1a69f308e56d7a",
+   "rev": "48375eac3aa5e3be2869d718e1f5c38b83787243",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "bump/v4.6.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",

diff --git a/lakefile.lean b/lakefile.lean
@@ -26,9 +26,9 @@ 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" @ "4f632e6fac86f6c3b7d4ac127c0ce8b06ab86f63"
+require std from git "https://github.com/leanprover/std4" @ "bump/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 aesop from git "https://github.com/leanprover-community/aesop" @ "bump/v4.6.0"
 require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4" @ "v0.0.25"
 require Cli from git "https://github.com/leanprover/lean4-cli" @ "main"
 

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-12-22
+leanprover/lean4:nightly-2023-12-31