From e085f343648445d935395b994283c4cb06410bb9 Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Sun, 30 Aug 2026 09:11:52 +0000 Subject: [PATCH 1/3] downstream: follow upstream PR --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index b8f3deceb..c0af3ac22 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-08-27 +leanprover/lean4-pr-releases:pr-release-14970-f51ba22 From 8f7063565eb4bd9b4ceca276892083f1f3b6fb01 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 30 Aug 2026 09:28:46 +0000 Subject: [PATCH 2/3] batteries+mathlib4: adapt to the new `CoreM` reader layer --- batteries/Batteries/Lean/LawfulMonad.lean | 2 +- mathlib4/Mathlib/Lean/Meta/RefinedDiscrTree/Initialize.lean | 3 ++- mathlib4/Mathlib/Tactic/ClickSuggestions/SectionState.lean | 4 ++-- 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/batteries/Batteries/Lean/LawfulMonad.lean b/batteries/Batteries/Lean/LawfulMonad.lean index 221b9c885..e6e097258 100644 --- a/batteries/Batteries/Lean/LawfulMonad.lean +++ b/batteries/Batteries/Lean/LawfulMonad.lean @@ -31,7 +31,7 @@ instance : LawfulMonad BaseIO := inferInstanceAs <| LawfulMonad (ST _) instance : LawfulMonad IO := inferInstanceAs <| LawfulMonad (EIO _) instance : LawfulMonad CoreM := - inferInstanceAs <| LawfulMonad (ReaderT _ <| StateRefT' _ _ (EIO Exception)) + inferInstanceAs <| LawfulMonad (ReaderT _ <| ReaderT _ <| StateRefT' _ _ (EIO Exception)) instance : LawfulMonad MetaM := inferInstanceAs <| LawfulMonad (ReaderT _ <| StateRefT' _ _ CoreM) instance : LawfulMonad TermElabM := diff --git a/mathlib4/Mathlib/Lean/Meta/RefinedDiscrTree/Initialize.lean b/mathlib4/Mathlib/Lean/Meta/RefinedDiscrTree/Initialize.lean index c7d0506df..b5ca93d33 100644 --- a/mathlib4/Mathlib/Lean/Meta/RefinedDiscrTree/Initialize.lean +++ b/mathlib4/Mathlib/Lean/Meta/RefinedDiscrTree/Initialize.lean @@ -142,7 +142,8 @@ Note: It is expensive to create two new `IO.Ref`s for every `MetaM` operation, -- mstate.modify fun s => { cache := s.cache } -- cstate.modify fun s => { env := s.env, cache := s.cache, ngen := s.ngen } let mctx := { keyedConfig := Config.toConfigWithKey { transparency := .reducible } } - match ← (((act name constInfo) mctx mstate) cctx cstate).toBaseIO with + -- `0` is the initial recursion depth of `CoreM`'s recursion-depth reader layer + match ← (((act name constInfo) mctx mstate) cctx 0 cstate).toBaseIO with | .ok a => return a.foldl (fun t (val, entries) => entries.foldl (fun t (key, entry) => t.push key (entry, val)) t) tree diff --git a/mathlib4/Mathlib/Tactic/ClickSuggestions/SectionState.lean b/mathlib4/Mathlib/Tactic/ClickSuggestions/SectionState.lean index 1dd1f3752..b852be359 100644 --- a/mathlib4/Mathlib/Tactic/ClickSuggestions/SectionState.lean +++ b/mathlib4/Mathlib/Tactic/ClickSuggestions/SectionState.lean @@ -79,8 +79,8 @@ where def SectionState.insertResult (s : SectionState α) (res : Result α) (isDup : α → α → MetaM Bool) : MetaM (SectionState α) := do let { results, errors } := s - let results ← fun c₁ c₂ c₃ c₄ ↦ - (res.insertInArray results isDup c₁ c₂ c₃ c₄).catchExceptions fun ex ↦ do + let results ← fun c₁ c₂ c₃ c₄ c₅ ↦ + (res.insertInArray results isDup c₁ c₂ c₃ c₄ c₅).catchExceptions fun ex ↦ do if let .internal id _ := ex then if id == interruptExceptionId then return default From a71541fc5ce1ae8605280fd176f3eeb28019c13c Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Mon, 31 Aug 2026 17:25:35 +0000 Subject: [PATCH 3/3] downstream: follow upstream PR --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index c0af3ac22..b4014a58e 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-14970-f51ba22 +leanprover/lean4-pr-releases:pr-release-14970-08499f9