Merge upstream/master into kim/to-dual-ccl-extended

Resolve merge conflicts with master's ConditionallyCompletePartialOrder
refactoring (PR leanprover-community#35047). The @[to_dual] annotations added by this branch
in CCL/Basic.lean, CCL/Indexed.lean, CCL/Finset.lean, and CCL/Group.lean
are incompatible with the new CCL→CCPO bridging instance, so these files
take master's versions. The @[to_dual] changes in CompleteLattice/Basic.lean
and all other files are preserved.

Conflicted files:
- Mathlib/Order/CompleteLattice/Basic.lean: kept branch's @[to_dual]
  additions and InfSet section removal; removed duplicate iInf_of_isEmpty
- Mathlib/Order/ConditionallyCompleteLattice/Basic.lean: took master's
  version (incompatible with @[to_dual] due to CCPO instance)
- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean: took master's
  version (same reason)

Also reverted to master for CCL/Finset.lean and CCL/Group.lean where
branch's @[to_dual existing] registrations conflict with the CCPO instance.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Author: kim-em

.github/workflows/actionlint.yml

@@ -16,4 +16,4 @@ jobs:
         uses: reviewdog/action-actionlint@e58ee9d111489c31395fbe4857b0be6e7635dbda # v1.70.0
         with:
           tool_name: actionlint
-          fail_level: error
+          fail_level: any

.github/workflows/build_template.yml

@@ -399,17 +399,12 @@ jobs:
           ../tools-branch/scripts/lake-build-with-retry.sh Counterexamples
           # results of build at pr-branch/.lake/build_summary_Counterexamples.json
 
-      - name: prepare cache staging directory
-        if: ${{ steps.build.outcome == 'success' }}
+      - name: stage Mathlib cache files
+        if: ${{ always() && (steps.build.outcome == 'success' || steps.build.outcome == 'failure' || steps.build.outcome == 'cancelled') }}
         shell: bash
         run: |
           rm -rf cache-staging
           mkdir -p cache-staging
-
-      - name: stage Mathlib cache files
-        if: ${{ steps.build.outcome == 'success' }}
-        shell: bash
-        run: |
           cd pr-branch
           lake env ../tools-branch/.lake/build/bin/cache --staging-dir="../cache-staging" stage
 
@@ -429,7 +424,7 @@ jobs:
 
       - name: check cache staging contents
         id: cache_staging_check
-        if: ${{ steps.build.outcome == 'success' }}
+        if: ${{ always() && (steps.build.outcome == 'success' || steps.build.outcome == 'failure' || steps.build.outcome == 'cancelled') }}
         shell: bash
         run: |
           if find cache-staging -type f -name '*.ltar' -print -quit | grep -q .; then
@@ -439,7 +434,7 @@ jobs:
           fi
 
       - name: upload cache staging artifact
-        if: ${{ steps.cache_staging_check.outputs.has_files == 'true' }}
+        if: ${{ always() && steps.cache_staging_check.outputs.has_files == 'true' }}
         uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6.0.0
         with:
           name: cache-staging
@@ -609,7 +604,7 @@ jobs:
     # We only upload the cache if the build started (whether succeeding, failing, or cancelled)
     # but not if any earlier step failed or was cancelled.
     # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Some.20files.20not.20found.20in.20the.20cache/near/407183836
-    if: ${{ always() && needs.build.outputs.build-outcome == 'success' && needs.build.outputs.get-cache-outcome == 'success' && needs.build.outputs.cache-staging-has-files == 'true' }}
+    if: ${{ always() && needs.build.outputs.cache-staging-has-files == 'true' }}
     steps:
       - name: Checkout tools branch
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
@@ -655,6 +650,7 @@ jobs:
   post_steps:
     name: Post-Build Step
     needs: [build, upload_cache]
+    if: ${{ always() && needs.build.result == 'success' && (needs.upload_cache.result == 'success' || needs.upload_cache.result == 'skipped') }}
     runs-on: ubuntu-latest # Note these steps run on disposable GitHub runners, so no landrun sandboxing is needed.
     steps:
 
@@ -744,7 +740,8 @@ jobs:
 
   final:
     name: Post-CI job
-    if: ${{ inputs.run_post_ci }}
+    # ensure that this runs iff direct dependencies succeeded even if transitive dependencies  were skipped
+    if: ${{ always() && inputs.run_post_ci && needs.style_lint.result == 'success' && needs.build.result == 'success' && needs.post_steps.result == 'success' }}
     needs: [style_lint, build, post_steps]
     runs-on: ubuntu-latest
     steps:

Archive/Wiedijk100Theorems/Konigsberg.lean

@@ -52,9 +52,7 @@ def graph : SimpleGraph Verts where
   symm := by
     dsimp [Symmetric, adj]
     decide
-  loopless := by
-    dsimp [Irreflexive, adj]
-    decide
+  loopless := ⟨by decide⟩
 
 instance : DecidableRel graph.Adj := fun a b => inferInstanceAs <| Decidable (adj a b)
 

Cache/IO.lean

@@ -390,13 +390,78 @@ def getLocalCacheSet : IO <| Std.TreeSet String compare := do
 def isFromMathlib (mod : Name) : Bool :=
   mod.getRoot == `Mathlib
 
+/-- Get the trace file path for a module. -/
+def getTracePath (mod : Name) : CacheM FilePath := do
+  let sp := (← read).srcSearchPath
+  let packageDir ← getSrcDir sp mod
+  let path := (System.mkFilePath <| mod.components.map toString)
+  return packageDir / LIBDIR / path.withExtension "trace"
+
+/-- Read the `depHash` from a trace file, if it exists and is valid.
+    Returns the hash as a UInt64. -/
+def readTraceHash (tracePath : FilePath) : IO (Option UInt64) := do
+  let contents ← try IO.FS.readFile tracePath
+                  catch _ => return none
+  -- Try to parse as JSON and extract depHash
+  let some json := Lean.Json.parse contents |>.toOption | return none
+  let some depHashStr := json.getObjValAs? String "depHash" |>.toOption | return none
+  -- Parse hex string to UInt64
+  return depHashStr.parseHexToUInt64?
+
+/-- Read the Lake depHash from an ltar file header.
+    The ltar format is: 4-byte magic (LTAR/LTR2/LTR3) + 8-byte little-endian u64 hash. -/
+def readLtarHash (ltarPath : FilePath) : IO (Option UInt64) := do
+  let some handle ← try
+      some <$> IO.FS.Handle.mk ltarPath .read
+    catch _ => pure none | return none
+  -- Read 12 bytes: 4 magic + 8 hash
+  let bytes ← handle.read 12
+  if bytes.size < 12 then return none
+  -- Verify magic (LTAR, LTR2, or LTR3)
+  let magic := String.fromUTF8! (bytes.extract 0 4)
+  if magic != "LTAR" && magic != "LTR2" && magic != "LTR3" then return none
+  -- Read little-endian u64 hash
+  let mut hash : UInt64 := 0
+  for i in [0:8] do
+    hash := hash ||| ((bytes.get! (4 + i)).toUInt64 <<< (i * 8).toUInt64)
+  return some hash
+
+/-- Check if a module's trace file indicates it is already decompressed with the correct hash.
+    The hash to compare comes from the ltar file header, not the mathlib cache hash.
+    Returns `true` if the module needs decompression, `false` if it can be skipped. -/
+def needsDecompression (mod : Name) (mathlibHash : UInt64) : CacheM Bool := do
+  -- Read the Lake depHash from the ltar file header
+  let ltarPath := CACHEDIR / mathlibHash.asLTar
+  let some ltarHash ← readLtarHash ltarPath | return true
+  -- Read the trace file hash
+  let tracePath ← getTracePath mod
+  let some traceHash ← readTraceHash tracePath | return true
+  -- They should match if the file is already decompressed
+  return ltarHash != traceHash
+
+/-- Filter the hashmap to only include modules that need decompression.
+    A module needs decompression if its trace file doesn't exist or has a different hash. -/
+def ModuleHashMap.filterNeedsDecompression (hashMap : ModuleHashMap) : CacheM ModuleHashMap :=
+  hashMap.foldM (init := ∅) fun acc mod hash => do
+    if ← needsDecompression mod hash then
+      return acc.insert mod hash
+    else
+      return acc
+
 /-- Decompresses build files into their respective folders -/
 def unpackCache (hashMap : ModuleHashMap) (force : Bool) : CacheM Unit := do
   let hashMap ← hashMap.filterExists true
+  let totalCached := hashMap.size
+  -- Unless force is set, filter to only modules that actually need decompression
+  let hashMap ← if force then pure hashMap else hashMap.filterNeedsDecompression
   let size := hashMap.size
+  let skipped := totalCached - size
   if size > 0 then
     let now ← IO.monoMsNow
-    IO.println s!"Decompressing {size} file(s)"
+    if skipped > 0 then
+      IO.println s!"Decompressing {size} file(s) ({skipped} already decompressed)"
+    else
+      IO.println s!"Decompressing {size} file(s)"
     let args := (if force then #["-f"] else #[]) ++ #["-x", "--delete-corrupted", "-j", "-"]
     let child ← IO.Process.spawn { cmd := ← getLeanTar, args, stdin := .piped }
     let (stdin, child) ← child.takeStdin
@@ -427,9 +492,12 @@ def unpackCache (hashMap : ModuleHashMap) (force : Bool) : CacheM Unit := do
     stdin.putStr <| Lean.Json.compress <| .arr config
     let exitCode ← child.wait
     if exitCode != 0 then throw <| IO.userError s!"leantar failed with error code {exitCode}"
-    IO.println s!"Unpacked in {(← IO.monoMsNow) - now} ms"
+    IO.println s!"Decompressed in {(← IO.monoMsNow) - now} ms"
     IO.println "Completed successfully!"
-  else IO.println "No cache files to decompress"
+  else if totalCached > 0 then
+    IO.println s!"Already decompressed {totalCached} file(s)"
+  else
+    IO.println "No cache files to decompress"
 
 instance : Ord FilePath where
   compare x y := compare x.toString y.toString

Cache/Lean.lean

@@ -28,6 +28,22 @@ def Nat.toHexDigits (n : Nat) : Nat → (res : String := "") → String
 def UInt64.asLTar (n : UInt64) : String :=
   s!"{Nat.toHexDigits n.toNat 8}.ltar"
 
+/-- Parse a single hex digit character to its numeric value. -/
+def Char.hexDigitToNat? (c : Char) : Option Nat :=
+  if '0' ≤ c ∧ c ≤ '9' then some (c.toNat - '0'.toNat)
+  else if 'a' ≤ c ∧ c ≤ 'f' then some (c.toNat - 'a'.toNat + 10)
+  else if 'A' ≤ c ∧ c ≤ 'F' then some (c.toNat - 'A'.toNat + 10)
+  else none
+
+/-- Parse a 16-character hex string (like "4bd6700ff435e8d0") to a UInt64. -/
+def String.parseHexToUInt64? (s : String) : Option UInt64 := do
+  if s.length != 16 then failure
+  let mut result : UInt64 := 0
+  for c in s.toList do
+    let digit ← c.hexDigitToNat?
+    result := (result <<< 4) ||| digit.toUInt64
+  return result
+
 -- copied from Mathlib
 /-- Create a `Name` from a list of components. -/
 def Lean.Name.fromComponents : List Name → Name := go .anonymous where

Mathlib.lean

@@ -1297,8 +1297,12 @@ public import Mathlib.AlgebraicGeometry.Fiber
 public import Mathlib.AlgebraicGeometry.FunctionField
 public import Mathlib.AlgebraicGeometry.GammaSpecAdjunction
 public import Mathlib.AlgebraicGeometry.Geometrically.Basic
+public import Mathlib.AlgebraicGeometry.Geometrically.Integral
+public import Mathlib.AlgebraicGeometry.Geometrically.Irreducible
+public import Mathlib.AlgebraicGeometry.Geometrically.Reduced
 public import Mathlib.AlgebraicGeometry.Gluing
 public import Mathlib.AlgebraicGeometry.GluingOneHypercover
+public import Mathlib.AlgebraicGeometry.Group.Abelian
 public import Mathlib.AlgebraicGeometry.Group.Smooth
 public import Mathlib.AlgebraicGeometry.IdealSheaf.Basic
 public import Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
@@ -1334,6 +1338,7 @@ public import Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
 public import Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
 public import Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
 public import Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
+public import Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
 public import Mathlib.AlgebraicGeometry.Morphisms.Separated
 public import Mathlib.AlgebraicGeometry.Morphisms.Smooth
 public import Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
@@ -1512,6 +1517,7 @@ public import Mathlib.Analysis.Analytic.RadiusLiminf
 public import Mathlib.Analysis.Analytic.Uniqueness
 public import Mathlib.Analysis.Analytic.WithLp
 public import Mathlib.Analysis.Analytic.Within
+public import Mathlib.Analysis.AperiodicOrder.Delone.Basic
 public import Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
 public import Mathlib.Analysis.Asymptotics.Completion
 public import Mathlib.Analysis.Asymptotics.Defs
@@ -1757,6 +1763,7 @@ public import Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
 public import Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
 public import Mathlib.Analysis.ConstantSpeed
 public import Mathlib.Analysis.Convex.AmpleSet
+public import Mathlib.Analysis.Convex.Approximation
 public import Mathlib.Analysis.Convex.Basic
 public import Mathlib.Analysis.Convex.Between
 public import Mathlib.Analysis.Convex.BetweenList
@@ -2647,6 +2654,7 @@ public import Mathlib.CategoryTheory.Limits.FinallySmall
 public import Mathlib.CategoryTheory.Limits.FintypeCat
 public import Mathlib.CategoryTheory.Limits.FormalCoproducts
 public import Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
+public import Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
 public import Mathlib.CategoryTheory.Limits.Fubini
 public import Mathlib.CategoryTheory.Limits.FullSubcategory
 public import Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
@@ -2657,6 +2665,7 @@ public import Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Images
 public import Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Kernels
 public import Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products
 public import Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
+public import Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Terminal
 public import Mathlib.CategoryTheory.Limits.FunctorToTypes
 public import Mathlib.CategoryTheory.Limits.HasLimits
 public import Mathlib.CategoryTheory.Limits.IndYoneda
@@ -3160,6 +3169,7 @@ public import Mathlib.CategoryTheory.Sites.Pullback
 public import Mathlib.CategoryTheory.Sites.RegularEpi
 public import Mathlib.CategoryTheory.Sites.Sheaf
 public import Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
+public import Mathlib.CategoryTheory.Sites.SheafCohomology.Cech
 public import Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris
 public import Mathlib.CategoryTheory.Sites.SheafHom
 public import Mathlib.CategoryTheory.Sites.SheafOfTypes
@@ -4267,6 +4277,7 @@ public import Mathlib.FieldTheory.Tower
 public import Mathlib.Geometry.Convex.Cone.Basic
 public import Mathlib.Geometry.Convex.Cone.Dual
 public import Mathlib.Geometry.Convex.Cone.Pointed
+public import Mathlib.Geometry.Convex.Cone.Simplicial
 public import Mathlib.Geometry.Convex.Cone.TensorProduct
 public import Mathlib.Geometry.Diffeology.Basic
 public import Mathlib.Geometry.Euclidean.Altitude
@@ -4688,6 +4699,7 @@ public import Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
 public import Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
 public import Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
 public import Mathlib.LinearAlgebra.ExteriorPower.Basic
+public import Mathlib.LinearAlgebra.ExteriorPower.Basis
 public import Mathlib.LinearAlgebra.ExteriorPower.Pairing
 public import Mathlib.LinearAlgebra.FiniteDimensional.Basic
 public import Mathlib.LinearAlgebra.FiniteDimensional.Defs
@@ -5582,7 +5594,9 @@ public import Mathlib.Order.ConditionallyCompleteLattice.Defs
 public import Mathlib.Order.ConditionallyCompleteLattice.Finset
 public import Mathlib.Order.ConditionallyCompleteLattice.Group
 public import Mathlib.Order.ConditionallyCompleteLattice.Indexed
+public import Mathlib.Order.ConditionallyCompletePartialOrder.Basic
 public import Mathlib.Order.ConditionallyCompletePartialOrder.Defs
+public import Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
 public import Mathlib.Order.Copy
 public import Mathlib.Order.CountableDenseLinearOrder
 public import Mathlib.Order.Cover
@@ -5820,6 +5834,7 @@ public import Mathlib.Probability.Decision.Risk.Basic
 public import Mathlib.Probability.Decision.Risk.Defs
 public import Mathlib.Probability.Density
 public import Mathlib.Probability.Distributions.Beta
+public import Mathlib.Probability.Distributions.Cauchy
 public import Mathlib.Probability.Distributions.Exponential
 public import Mathlib.Probability.Distributions.Fernique
 public import Mathlib.Probability.Distributions.Gamma

Mathlib/Algebra/Algebra/Defs.lean

@@ -404,14 +404,6 @@ lemma algebraMap_self_apply (x : R) : algebraMap R R x = x := rfl
 
 namespace id
 
-@[deprecated algebraMap_self (since := "2025-07-17")]
-theorem map_eq_id : algebraMap R R = RingHom.id _ :=
-  rfl
-
-@[deprecated algebraMap_self_apply (since := "2025-07-17")]
-theorem map_eq_self (x : R) : algebraMap R R x = x :=
-  rfl
-
 @[deprecated _root_.smul_eq_mul (since := "2025-12-02")]
 theorem smul_eq_mul (x y : R) : x • y = x * y :=
   rfl

Mathlib/Algebra/Category/Grp/Limits.lean

@@ -147,7 +147,7 @@ instance hasLimitsOfShape [Small.{u} J] : HasLimitsOfShape J GrpCat.{u} where
   has_limit _ := inferInstance
 
 /-- The category of groups has all limits. -/
-@[to_additive (relevant_arg := _) /-- The category of additive groups has all limits. -/]
+@[to_additive /-- The category of additive groups has all limits. -/]
 instance hasLimitsOfSize [UnivLE.{v, u}] : HasLimitsOfSize.{w, v} GrpCat.{u} where
   has_limits_of_shape J _ := { }
 
@@ -159,7 +159,7 @@ instance hasLimits : HasLimits GrpCat.{u} :=
 
 This means the underlying monoid of a limit can be computed as a limit in the category of monoids.
 -/
-@[to_additive (relevant_arg := _) AddGrpCat.forget₂AddMonPreservesLimitsOfSize
+@[to_additive AddGrpCat.forget₂AddMonPreservesLimitsOfSize
 /-- The forgetful functor from additive groups to additive monoids preserves all limits.
 
 This means the underlying additive monoid of a limit can be computed as a limit in the category of
@@ -183,7 +183,7 @@ instance forget_preservesLimitsOfShape [Small.{u} J] :
 /-- The forgetful functor from groups to types preserves all limits.
 
 This means the underlying type of a limit can be computed as a limit in the category of types. -/
-@[to_additive (relevant_arg := _)
+@[to_additive
 /-- The forgetful functor from additive groups to types preserves all limits.
 
 This means the underlying type of a limit can be computed as a limit in the category of types. -/]
@@ -207,7 +207,7 @@ noncomputable instance forget_createsLimitsOfShape :
 
 /-- The forgetful functor from groups to types creates all limits.
 -/
-@[to_additive (relevant_arg := _)
+@[to_additive
 /-- The forgetful functor from additive groups to types creates all limits. -/]
 noncomputable instance forget_createsLimitsOfSize :
     CreatesLimitsOfSize.{w, v} (forget GrpCat.{u}) where
@@ -315,7 +315,7 @@ instance hasLimitsOfShape [Small.{u} J] : HasLimitsOfShape J CommGrpCat.{u} wher
   has_limit _ := inferInstance
 
 /-- The category of commutative groups has all limits. -/
-@[to_additive (relevant_arg := _)
+@[to_additive
 /-- The category of additive commutative groups has all limits. -/]
 instance hasLimitsOfSize [UnivLE.{v, u}] : HasLimitsOfSize.{w, v} CommGrpCat.{u} where
   has_limits_of_shape _ _ := { }
@@ -343,7 +343,7 @@ instance forget₂Group_preservesLimitsOfShape :
 (That is, the underlying group could have been computed instead as limits in the category
 of groups.)
 -/
-@[to_additive (relevant_arg := _)
+@[to_additive
 /-- The forgetful functor from additive commutative groups to additive groups preserves all
 limits. (That is, the underlying group could have been computed instead as limits in the
 category of additive groups.) -/]
@@ -427,7 +427,7 @@ noncomputable instance forget_createsLimitsOfShape (J : Type v) [Category.{w} J]
 
 /-- The forgetful functor from commutative groups to types creates all limits.
 -/
-@[to_additive (relevant_arg := _)
+@[to_additive
 /-- The forgetful functor from additive commutative groups to types creates all limits. -/]
 noncomputable instance forget_createsLimitsOfSize :
     CreatesLimitsOfSize.{w, v} (forget CommGrpCat.{u}) where