chore: adaptations for nightly-2025-12-10

Author: kim-em

Mathlib/Tactic/Linter/TextBased.lean

@@ -262,7 +262,7 @@ def nonbreakingSpaceLinter : TextbasedLinter := fun opts lines ↦ Id.run do
   for h : idx in [:lines.size] do
     let line := lines[idx]
     let pos := line.find (· == ' ')
-    if pos != line.rawEndPos then
+    if pos != line.endPos then
       errors := errors.push (StyleError.nonbreakingSpace, idx + 1)
   return (errors, none)
 

lake-manifest.json

@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "bda61ace1e2fbf73689899a8b3ca5fc74b0e21b1",
+   "rev": "80627bbde8b8a0474814092e1dd2aff89123cc1a",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",

lakefile.lean

@@ -177,7 +177,7 @@ update its toolchain to match Mathlib's and fetch the new cache.
 -/
 post_update pkg do
   let rootPkg ← getRootPackage
-  if rootPkg.name = pkg.name then
+  if rootPkg.baseName = pkg.baseName then
     return -- do not run in Mathlib itself
   if (← IO.getEnv "MATHLIB_NO_CACHE_ON_UPDATE") != some "1" then
     -- Check if Lake version matches toolchain version
@@ -204,4 +204,4 @@ post_update pkg do
     finally
       IO.Process.setCurrentDir cwd
     if exitCode ≠ 0 then
-      error s!"{pkg.name}: failed to fetch cache"
+      error s!"{pkg.baseName}: failed to fetch cache"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2025-12-09
+leanprover/lean4:nightly-2025-12-10