Merge remote-tracking branch 'upstream/master' into kim/to-dual-fixed-points

# Conflicts:
#	Mathlib/Order/CompleteLattice/Basic.lean
#	Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
#	Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean

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:

.github/workflows/zulip_emoji_ci_status.yaml

@@ -0,0 +1,101 @@
+name: Zulip emoji CI status
+
+on:
+  workflow_run:
+    workflows: ["continuous integration", "continuous integration (mathlib forks)"]
+    types: [requested, completed]
+
+# Limit permissions for GITHUB_TOKEN for the entire workflow
+permissions:
+  contents: read
+  pull-requests: read
+  # All other permissions are implicitly 'none'
+
+jobs:
+  update_ci_emoji:
+    runs-on: ubuntu-latest
+    if: github.repository == 'leanprover-community/mathlib4'
+    steps:
+    - name: Determine PR number
+      id: pr
+      env:
+        GH_TOKEN: ${{ github.token }}
+        HEAD_BRANCH: ${{ github.event.workflow_run.head_branch }}
+        HEAD_REPO_OWNER: ${{ github.event.workflow_run.head_repository.owner.login }}
+        HEAD_SHA: ${{ github.event.workflow_run.head_sha }}
+      run: |
+        # Try to get PR number from the workflow_run event
+        PR_NUMBER=$(echo '${{ toJSON(github.event.workflow_run.pull_requests) }}' | jq -r '.[0].number // empty')
+        # For push-triggered CI (non-fork PRs), pull_requests may be empty;
+        # fall back to looking up the PR by branch name.
+        # Use owner:branch format to avoid matching the wrong PR when
+        # multiple forks use the same branch name.
+        if [ -z "$PR_NUMBER" ]; then
+          PR_NUMBER=$(gh pr list --repo "${{ github.repository }}" --head "$HEAD_REPO_OWNER:$HEAD_BRANCH" --state open --json number,headRefOid --jq ".[] | select(.headRefOid == \"$HEAD_SHA\") | .number" 2>/dev/null || true)
+        fi
+        # If owner-qualified lookup failed, try without owner (for same-repo branches)
+        if [ -z "$PR_NUMBER" ]; then
+          PR_NUMBER=$(gh pr list --repo "${{ github.repository }}" --head "$HEAD_BRANCH" --state open --json number,headRefOid --jq ".[] | select(.headRefOid == \"$HEAD_SHA\") | .number" 2>/dev/null || true)
+        fi
+        if [ -z "$PR_NUMBER" ]; then
+          echo "No PR found for branch $HEAD_REPO_OWNER:$HEAD_BRANCH at $HEAD_SHA, skipping"
+          echo "skip=true" >> "$GITHUB_OUTPUT"
+        else
+          echo "Found PR #$PR_NUMBER"
+          echo "pr_number=$PR_NUMBER" >> "$GITHUB_OUTPUT"
+          echo "skip=false" >> "$GITHUB_OUTPUT"
+        fi
+
+    - name: Determine CI action
+      id: action
+      if: steps.pr.outputs.skip != 'true'
+      run: |
+        EVENT_ACTION="${{ github.event.action }}"
+        CONCLUSION="${{ github.event.workflow_run.conclusion }}"
+        echo "Event action: $EVENT_ACTION, conclusion: $CONCLUSION"
+        if [ "$EVENT_ACTION" = "requested" ]; then
+          echo "ci_action=ci-running" >> "$GITHUB_OUTPUT"
+        elif [ "$EVENT_ACTION" = "completed" ]; then
+          case "$CONCLUSION" in
+            success)
+              echo "ci_action=ci-success" >> "$GITHUB_OUTPUT"
+              ;;
+            cancelled)
+              # Clear the running emoji. A new run may or may not follow
+              # (manual cancel, branch deleted, etc.), so don't leave stale 🟡.
+              echo "ci_action=ci-cancelled" >> "$GITHUB_OUTPUT"
+              ;;
+            *)
+              echo "ci_action=ci-failure" >> "$GITHUB_OUTPUT"
+              ;;
+          esac
+        fi
+
+    - name: Checkout mathlib repository
+      if: steps.pr.outputs.skip != 'true' && steps.action.outputs.ci_action != 'skip'
+      uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+      with:
+        ref: master
+        sparse-checkout: |
+          scripts/zulip_emoji_reactions.py
+
+    - name: Set up Python
+      if: steps.pr.outputs.skip != 'true' && steps.action.outputs.ci_action != 'skip'
+      uses: actions/setup-python@a309ff8b426b58ec0e2a45f0f869d46889d02405 # v6.2.0
+      with:
+        python-version: '3.x'
+
+    - name: Install dependencies
+      if: steps.pr.outputs.skip != 'true' && steps.action.outputs.ci_action != 'skip'
+      run: |
+        python -m pip install --upgrade pip
+        pip install zulip
+
+    - name: Update CI emoji
+      if: steps.pr.outputs.skip != 'true' && steps.action.outputs.ci_action != 'skip'
+      env:
+        ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
+        ZULIP_EMAIL: github-mathlib4-bot@leanprover.zulipchat.com
+        ZULIP_SITE: https://leanprover.zulipchat.com
+      run: |
+        python scripts/zulip_emoji_reactions.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "${{ steps.action.outputs.ci_action }}" "none" "${{ steps.pr.outputs.pr_number }}"

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