Update lean-toolchain for leanprover/lean4#10967

Author: leanprover-community-mathlib4-bot

Batteries/Lean/SatisfiesM.lean

@@ -21,18 +21,12 @@ open Lean Elab Term Tactic Command
 -- Note: as of nightly-2025-10-23, after https://github.com/leanprover/lean4/pull/10625
 -- these instances need to be re-implemented.
 
--- instance : MonadSatisfying (ST σ) where
---   satisfying {α p x} h := sorry
---   val_eq h := sorry
-
--- instance : MonadSatisfying (EST ε σ) where
---   satisfying h := sorry
---   val_eq h := sorry
-
--- instance : MonadSatisfying (EIO ε) := inferInstanceAs <| MonadSatisfying (EST _ _)
--- instance : MonadSatisfying BaseIO := inferInstanceAs <| MonadSatisfying (ST _)
+-- instance : MonadSatisfying (EIO ε) := inferInstanceAs <| MonadSatisfying (EStateM _ _)
+-- instance : MonadSatisfying BaseIO := inferInstanceAs <| MonadSatisfying (EIO _)
 -- instance : MonadSatisfying IO := inferInstanceAs <| MonadSatisfying (EIO _)
 
+-- instance : MonadSatisfying (EST ε σ) := inferInstanceAs <| MonadSatisfying (EStateM _ _)
+
 -- instance : MonadSatisfying CoreM :=
 --   inferInstanceAs <| MonadSatisfying (ReaderT _ <| StateRefT' _ _ (EIO _))
 

lakefile.toml

@@ -6,7 +6,10 @@ defaultTargets = ["Batteries", "runLinter"]
 [leanOptions]
 linter.missingDocs = true
 experimental.module = true
-backward.privateInPublic.warn = false
+# We prefix this with `weak.` so that running `lake new my_project math`
+# with an older default toolchain doesn't fail when running the Mathlib post update hook.
+# This option should be removed entirely once Batteries stops using `backward.privateInPublic`.
+weak.backward.privateInPublic.warn = false
 
 [[lean_lib]]
 name = "Batteries"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4-pr-releases:pr-release-10967-e7a43ff
+leanprover/lean4-pr-releases:pr-release-10967-905c960