chore: adaptations for nightly-2026-05-10 (#219)

Author: kim-em

Cache/IO.lean

@@ -503,8 +503,6 @@ def lookup (hashMap : ModuleHashMap) (modules : List Name) : IO Unit := do
       println! "  comment: {line}"
   if err then IO.Process.exit 1
 
-open private Lake.Glob.ofString? from Lake.Load.Toml in
-
 /--
 Parse a string as either a path or a Lean module name.
 If the argument describes a folder, use `walkDir` to find all `.lean` files within.

Mathlib/Data/String/Lemmas.lean

@@ -28,10 +28,10 @@ lemma length_eq_list_length (l : List Char) : (String.ofList l).length = l.lengt
   to the larger of `n` and `s.length` -/
 @[simp] lemma length_leftpad (n : ℕ) (c : Char) :
     ∀ (s : String), (leftpad n c s).length = max n s.length
-  | s => by simp [leftpad, Nat.sub_add_eq_max]
+  | s => by simp [leftpad, length_toList, Nat.sub_add_eq_max]
 
 lemma leftpad_prefix (n : ℕ) (c : Char) : ∀ s, IsPrefix (replicate (n - length s) c) (leftpad n c s)
-  | s => by simp [leftpad, IsPrefix, replicate]
+  | s => by simp [leftpad, IsPrefix, replicate, length_toList]
 
 lemma leftpad_suffix (n : ℕ) (c : Char) : ∀ s, IsSuffix s (leftpad n c s)
   | s => by simp [leftpad, IsSuffix]

lake-manifest.json

@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "cdab3938ccabbdb044be6896e251b5814bec932e",
+   "rev": "fd70b40073aeca8fa60fe0fb492f189d3b12c0ef",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "25a8b1685158cc5b463b2cdf3d06f16846a3b919",
+   "rev": "8e1db9dde3100736e39943b355d076c6f3b38fff",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2026-05-07
+leanprover/lean4:nightly-2026-05-10