chore: merge bump/v4.25.0 (leanprover-community#30740)

Author: kim-em

.github/workflows/nightly-docgen.yml

@@ -57,7 +57,7 @@ jobs:
           [[require]]
           scope = "leanprover"
           name = "doc-gen4"
-          rev = "main"
+          rev = "nightly-testing"
           EOF
 
           # Initialise docbuild as a Lean project

Cache/IO.lean

@@ -70,7 +70,7 @@ def CURLBIN :=
 
 /-- leantar version at https://github.com/digama0/leangz -/
 def LEANTARVERSION :=
-  "0.1.15"
+  "0.1.16-pre3"
 
 def EXE := if System.Platform.isWindows then ".exe" else ""
 
@@ -90,7 +90,7 @@ def getLeanTar : IO String := do
 /-- Bump this number to invalidate the cache, in case the existing hashing inputs are insufficient.
 It is not a global counter, and can be reset to 0 as long as the lean githash or lake manifest has
 changed since the last time this counter was touched. -/
-def rootHashGeneration : UInt64 := 0
+def rootHashGeneration : UInt64 := 1
 
 /--
 `CacheM` stores the following information:
@@ -311,12 +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 "extra", false)]
 
 /-- Check that all required build files exist. -/

Cache/Requests.lean

@@ -31,7 +31,7 @@ def extractRepoFromUrl (url : String) : Option String := do
   let url := url.stripSuffix ".git"
   let pos ← url.revFind (· == '/')
   let pos ← url.revFindAux (fun c => c == '/'  || c == ':') pos
-  return url.extract (url.next pos) url.endPos
+  return (String.Pos.Raw.extract url) (String.Pos.Raw.next url pos) url.endPos
 
 /-- Spot check if a URL is valid for a git remote -/
 def isRemoteURL (url : String) : Bool :=
@@ -81,12 +81,12 @@ def findMathlibRemote (mathlibDepPath : FilePath) : IO String := do
       Ensure Git is installed.\n\
       Stdout:\n{remotesInfo.stdout.trim}\nStderr:\n{remotesInfo.stderr.trim}\n"
 
-  let remoteLines := remotesInfo.stdout.split (· == '\n')
+  let remoteLines := remotesInfo.stdout.splitToList (· == '\n')
   let mut mathlibRemote : Option String := none
   let mut originPointsToMathlib : Bool := false
 
   for line in remoteLines do
-    let parts := line.trim.split (· == '\t')
+    let parts := line.trim.splitToList (· == '\t')
     if parts.length >= 2 then
       let remoteName := parts[0]!
       let remoteUrl := parts[1]!.takeWhile (· != ' ') -- Remove (fetch) or (push) suffix
@@ -115,7 +115,7 @@ def findMathlibRemote (mathlibDepPath : FilePath) : IO String := do
 Extracts PR number from a git ref like "refs/remotes/upstream/pr/1234"
 -/
 def extractPRNumber (ref : String) : Option Nat := do
-  let parts := ref.split (· == '/')
+  let parts := ref.splitToList (· == '/')
   if parts.length >= 2 && parts[parts.length - 2]! == "pr" then
     let prStr := parts[parts.length - 1]!
     prStr.toNat?

Mathlib.lean

@@ -4153,6 +4153,7 @@ import Mathlib.InformationTheory.KullbackLeibler.KLFun
 import Mathlib.Init
 import Mathlib.Lean.ContextInfo
 import Mathlib.Lean.CoreM
+import Mathlib.Lean.Elab.InfoTree
 import Mathlib.Lean.Elab.Tactic.Basic
 import Mathlib.Lean.Elab.Tactic.Meta
 import Mathlib.Lean.Elab.Term

Mathlib/Algebra/Algebra/StrictPositivity.lean

@@ -60,7 +60,7 @@ lemma _root_.IsUnit.isStrictlyPositive [LE A] [Monoid A] [Zero A]
 lemma isSelfAdjoint [Semiring A] [PartialOrder A] [StarRing A] [StarOrderedRing A] {a : A}
     (ha : IsStrictlyPositive a) : IsSelfAdjoint a := ha.nonneg.isSelfAdjoint
 
-@[simp, grind]
+@[simp, grind .]
 lemma _root_.isStrictlyPositive_one [LE A] [Monoid A] [Zero A] [ZeroLEOneClass A] :
     IsStrictlyPositive (1 : A) := iff_of_unital.mpr ⟨zero_le_one, isUnit_one⟩
 

Mathlib/Algebra/BigOperators/Group/List/Basic.lean

@@ -53,7 +53,7 @@ theorem prod_concat : (l.concat a).prod = l.prod * a := by
 theorem prod_flatten {l : List (List M)} : l.flatten.prod = (l.map List.prod).prod := by
   induction l with
   | nil => simp
-  | cons head tail ih => simp only [*, List.flatten, map, prod_append, prod_cons]
+  | cons head tail ih => simp only [*, List.flatten_cons, map, prod_append, prod_cons]
 
 open scoped Relator in
 @[to_additive]

Mathlib/Algebra/BigOperators/Group/List/Lemmas.lean

@@ -138,7 +138,7 @@ lemma drop_take_succ_flatten_eq_getElem (L : List (List α)) (i : Nat) (h : i <
   have : (L.map length).take i = ((L.take (i + 1)).map length).take i := by
     simp [map_take, take_take, Nat.min_eq_left]
   simp only [this, take_sum_flatten, drop_sum_flatten,
-    drop_take_succ_eq_cons_getElem, h, flatten, append_nil]
+    drop_take_succ_eq_cons_getElem, h, flatten_nil, flatten_cons, append_nil]
 
 end List
 

Mathlib/Algebra/Notation/Defs.lean

@@ -74,10 +74,6 @@ attribute [to_additive existing (reorder := 1 2, 5 6) hSMul] HPow.hPow
 attribute [to_additive existing (reorder := 1 2, 4 5) smul] Pow.pow
 
 attribute [to_additive (attr := default_instance)] instHSMul
-
-@[to_additive]
-theorem SMul.smul_eq_hSMul {α β} [SMul α β] : (SMul.smul : α → β → β) = HSMul.hSMul := rfl
-
 attribute [to_additive existing (reorder := 1 2)] instHPow
 
 variable {G : Type*}

Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean

@@ -120,7 +120,10 @@ instance : AddLeftMono ℚ where
 
 theorem div_lt_div_iff_mul_lt_mul {a b c d : ℤ} (b_pos : 0 < b) (d_pos : 0 < d) :
     (a : ℚ) / b < c / d ↔ a * d < c * b := by
-  grind [lt_iff_le_not_ge, Rat.divInt_le_divInt, div_def', num_intCast, den_intCast]
+  simp only [lt_iff_le_not_ge]
+  apply and_congr
+  · simp [div_def', Rat.divInt_le_divInt b_pos d_pos]
+  · simp [div_def', Rat.divInt_le_divInt d_pos b_pos]
 
 theorem lt_one_iff_num_lt_denom {q : ℚ} : q < 1 ↔ q.num < q.den := by simp [Rat.lt_iff]
 

Mathlib/Algebra/Polynomial/RuleOfSigns.lean

@@ -244,6 +244,12 @@ private lemma exists_cons_of_leadingCoeff_pos (η) (h₁ : 0 < leadingCoeff P) (
     by_cases h₉ : ((X - C η) * P).nextCoeff = 0
     · suffices ((X - C η) * P).eraseLead = ((X - C η) * P.eraseLead).eraseLead by
         have := coeffList_eraseLead (mul_ne_zero (X_sub_C_ne_zero η) h₃)
+        #adaptation_note
+        /--
+        Moving from `nightly-2025-10-13` to `nightly-2025-10-19`
+        we now need to provide an intermediate step.
+        -/
+        have : ((X - C η) * P).natDegree - ((X - C η) * P).eraseLead.degree.succ = n + 1 := by grind
         grind [leadingCoeff_mul, leadingCoeff_X_sub_C]
       suffices C η * monomial P.natDegree P.leadingCoeff = monomial P.natDegree P.nextCoeff by
         grind [X_mul_monomial, sub_mul, mul_sub, self_sub_monomial_natDegree_leadingCoeff]