chore: adaptations for nightly-2025-10-20

Author: kim-em

Cache/IO.lean

@@ -70,7 +70,7 @@ def CURLBIN :=
 
 /-- leantar version at https://github.com/digama0/leangz -/
 def LEANTARVERSION :=
-  "0.1.16-pre2"
+  "0.1.16-pre3"
 
 def EXE := if System.Platform.isWindows then ".exe" else ""
 
@@ -311,18 +311,20 @@ def mkBuildPaths (mod : Name) : CacheM <| List (FilePath × Bool) := do
   return [
     -- Note that `packCache` below requires that the `.trace` file is first in this list.
     (packageDir / LIBDIR / path.withExtension "trace", true),
+    -- Note: the `.olean`, `.olean.server`, `.olean.private` files must be consecutive,
+    -- and in this order. The corresponding `.hash` files can come afterwards, in any order.
     (packageDir / LIBDIR / path.withExtension "olean", true),
+    (packageDir / LIBDIR / path.withExtension "olean.server", false),
+    (packageDir / LIBDIR / path.withExtension "olean.private", false),
     (packageDir / LIBDIR / path.withExtension "olean.hash", true),
+    (packageDir / LIBDIR / path.withExtension "olean.server.hash", false),
+    (packageDir / LIBDIR / path.withExtension "olean.private.hash", false),
     (packageDir / LIBDIR / path.withExtension "ilean", true),
     (packageDir / LIBDIR / path.withExtension "ilean.hash", true),
     (packageDir / IRDIR  / path.withExtension "c", true),
     (packageDir / IRDIR  / path.withExtension "c.hash", true),
     -- (packageDir / LIBDIR / path.withExtension "ir", true),
     -- (packageDir / LIBDIR / path.withExtension "ir.hash", true),
-    -- (packageDir / LIBDIR / path.withExtension "olean.private", false),
-    -- (packageDir / LIBDIR / path.withExtension "olean.private.hash", false),
-    -- (packageDir / LIBDIR / path.withExtension "olean.server", false),
-    -- (packageDir / LIBDIR / path.withExtension "olean.server.hash", false),
     (packageDir / LIBDIR / path.withExtension "extra", false)]
 
 /-- Check that all required build files exist. -/

Mathlib/Data/Set/Insert.lean

@@ -40,7 +40,12 @@ theorem insert_def (x : α) (s : Set α) : insert x s = { y | y = x ∨ y ∈ s
 @[simp]
 theorem subset_insert (x : α) (s : Set α) : s ⊆ insert x s := fun _ => Or.inr
 
-grind_pattern subset_insert => _ ⊆ insert x s
+-- This is a fairly aggressive pattern; it might be safer to use
+-- `s ⊆ insert x s` or `_ ⊆ insert x s` instead.
+-- Currently Cslib relies on this.
+-- See `MathlibTest/grind/set.lean` for a test case illustrating the reasoning
+-- that Cslib is relying on.
+grind_pattern subset_insert => insert x s
 
 theorem mem_insert (x : α) (s : Set α) : x ∈ insert x s :=
   Or.inl rfl

lake-manifest.json

@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "84b9c4f5f7f9ab594ca6252bf91e293b974cc29a",
+   "rev": "6de2dd4b6aac9ce8825fa93c2b99b5e06c0b5456",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "07d6ac02ebdf6ef77651c9e1750c179d0f609ee6",
+   "rev": "85cc6389e0566786b2966da9512d1e8cf2402d96",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8d6f25c325b16b3b8a6dee0f05d20e424fe1bc30",
+   "rev": "4ea21a7d20e5ac4db46bab6013b53edc109abd04",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -75,10 +75,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "b62fd39acc32da6fb8bb160c82d1bbc3cb3c186e",
+   "rev": "88e435f7b94b7e77c2006a72bf0702750684a8fb",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "nightly-testing",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "mathlib",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2025-10-19
+leanprover/lean4:nightly-2025-10-20