Merge branch 'master' into IsSemitopologicalRing

Author: j-loreaux

.github/workflows/build_template.yml

@@ -122,6 +122,7 @@ jobs:
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
         with:
           ref: ${{ inputs.pr_branch_ref }}
+          fetch-depth: 2 # we may fetch cache from the commit before this one (or earlier)
           path: pr-branch
 
       - name: Prepare DownstreamTest directory
@@ -337,21 +338,66 @@ jobs:
 
       - name: get cache (3/3 - finalize cache operation)
         id: get
-        shell: bash # only runs `cache get` from `tools-branch`, so doesn't need to be inside landrun
+        shell: bash # only runs git and `cache get` from `tools-branch`, so doesn't need to be inside landrun
+        env:
+          BEFORE_SHA: ${{ github.event.before || '' }}
+          BASE_SHA: ${{ github.event.pull_request.base.sha || '' }}
+          CACHE_REPO: ${{ github.event.pull_request.head.repo.full_name || github.repository }}
         run: |
           cd pr-branch
-          if [[ "${{ steps.get_cache_part2_test.outcome }}" == "success" ]]; then
-            echo "Fetching all remaining cache..."
+          if [[ "${{ steps.get_cache_part2_test.outcome }}" != "success" ]]; then
+            echo "WARNING: 'lake build --no-build -v Mathlib.Init' failed."
+            echo "No cache for 'Mathlib.Init' available or it could not be prepared."
+            exit 0
+          fi
 
-            ../tools-branch/.lake/build/bin/cache --skip-proofwidgets get
+          ORIG_SHA="$(git rev-parse HEAD)"
+          PREV_SHA=""
+          PREV_SHA_SOURCE=""
 
-            # Run again with --repo, to ensure we actually get the oleans.
-            ../tools-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} --skip-proofwidgets get
+          # When a ref is newly created, github.event.before can be all-zero.
+          if [[ "$BEFORE_SHA" =~ ^0{40}$ ]]; then
+            BEFORE_SHA=""
+          fi
+
+          if [[ -n "$BEFORE_SHA" ]]; then
+            PREV_SHA="$BEFORE_SHA"
+            PREV_SHA_SOURCE="github.event.before"
+          elif [[ -n "$BASE_SHA" ]]; then
+            PREV_SHA="$BASE_SHA"
+            PREV_SHA_SOURCE="pull_request.base.sha"
           else
-            echo "WARNING: 'lake build --no-build -v Mathlib.Init' failed."
-            echo "No cache for 'Mathlib.Init' available or it could not be prepared."
+            PREV_SHA="$(git rev-parse --verify --quiet HEAD^ || true)"
+            if [[ -n "$PREV_SHA" ]]; then
+              PREV_SHA_SOURCE="HEAD^"
+            fi
           fi
 
+          if [[ -n "$PREV_SHA" ]]; then
+            # cf. https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Mathlib.20has.20moved.20to.20the.20new.20module.20system/near/563452000
+            echo "Warming up cache using previous commit: $PREV_SHA (source: $PREV_SHA_SOURCE)"
+            if git cat-file -e "$PREV_SHA^{commit}" 2>/dev/null || git fetch --no-tags --depth=1 origin "$PREV_SHA"; then
+              git checkout "$PREV_SHA"
+              ../tools-branch/.lake/build/bin/cache --skip-proofwidgets get
+              # Run again with --repo, to ensure we actually get the oleans.
+              ../tools-branch/.lake/build/bin/cache --repo="$CACHE_REPO" --skip-proofwidgets get
+
+              echo "Switching back to branch head"
+              git checkout "$ORIG_SHA"
+            else
+              echo "Could not fetch $PREV_SHA; skipping parent warmup cache fetch."
+            fi
+          else
+            echo "No previous commit candidate found; skipping parent warmup cache fetch."
+          fi
+
+          echo "Fetching all remaining cache..."
+
+          ../tools-branch/.lake/build/bin/cache --skip-proofwidgets get
+
+          # Run again with --repo, to ensure we actually get the oleans.
+          ../tools-branch/.lake/build/bin/cache --repo="$CACHE_REPO" --skip-proofwidgets get
+
       - name: fetch ProofWidgets release
         # We need network access for ProofWidgets frontend assets.
         # Run inside landrun so PR-controlled code remains sandboxed.

.github/workflows/maintainer_bors_wf_run.yml

@@ -69,14 +69,21 @@ jobs:
       - name: Select bridge or legacy inputs
         id: inputs
         if: ${{ steps.bridge.outputs.pr_number != '' || steps.legacy.outputs.pr_number != '' }}
+        env:
+          INPUT_AUTHOR: ${{ steps.bridge.outputs.author }}${{ steps.legacy.outputs.author }}
+          INPUT_PR_NUMBER: ${{ steps.bridge.outputs.pr_number }}${{ steps.legacy.outputs.pr_number }}
+          INPUT_BOT: ${{ steps.bridge.outputs.bot }}${{ steps.legacy.outputs.bot }}
+          INPUT_REMOVE_LABELS: ${{ steps.bridge.outputs.removeLabels }}${{ steps.legacy.outputs.removeLabels }}
+          INPUT_MORD: ${{ steps.bridge.outputs.mOrD }}${{ steps.legacy.outputs.mOrD }}
+          INPUT_SOURCE: ${{ steps.bridge.outputs.pr_number != '' && 'bridge' || (steps.legacy.outputs.pr_number != '' && 'legacy' || 'none') }}
         run: |
           {
-            echo "author=${{ steps.bridge.outputs.author }}${{ steps.legacy.outputs.author }}"
-            echo "pr_number=${{ steps.bridge.outputs.pr_number }}${{ steps.legacy.outputs.pr_number }}"
-            echo "bot=${{ steps.bridge.outputs.bot }}${{ steps.legacy.outputs.bot }}"
-            echo "removeLabels=${{ steps.bridge.outputs.removeLabels }}${{ steps.legacy.outputs.removeLabels }}"
-            echo "mOrD=${{ steps.bridge.outputs.mOrD }}${{ steps.legacy.outputs.mOrD }}"
-            echo "input_source=${{ steps.bridge.outputs.pr_number != '' && 'bridge' || (steps.legacy.outputs.pr_number != '' && 'legacy' || 'none') }}"
+            echo "author=${INPUT_AUTHOR}"
+            echo "pr_number=${INPUT_PR_NUMBER}"
+            echo "bot=${INPUT_BOT}"
+            echo "removeLabels=${INPUT_REMOVE_LABELS}"
+            echo "mOrD=${INPUT_MORD}"
+            echo "input_source=${INPUT_SOURCE}"
           } | tee -a "$GITHUB_OUTPUT"
 
       - name: Note legacy artifact fallback
@@ -182,6 +189,7 @@ jobs:
         if: ${{ ! steps.inputs.outputs.mOrD == '' &&
           ( steps.user_permission.outputs.require-result == 'true' ||
             steps.inputs.outputs.bot == 'true' ) }}
+        continue-on-error: true
         env:
           ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
           ZULIP_EMAIL: github-mathlib4-bot@leanprover.zulipchat.com

.github/workflows/maintainer_merge_wf_run.yml

@@ -73,18 +73,28 @@ jobs:
       - name: Select bridge or legacy inputs
         id: inputs
         if: ${{ steps.bridge.outputs.pr_number != '' || steps.legacy.outputs.pr_number != '' }}
+        env:
+          INPUT_AUTHOR: ${{ steps.bridge.outputs.author }}${{ steps.legacy.outputs.author }}
+          INPUT_PR_AUTHOR: ${{ steps.bridge.outputs.pr_author }}${{ steps.legacy.outputs.pr_author }}
+          INPUT_PR_NUMBER: ${{ steps.bridge.outputs.pr_number }}${{ steps.legacy.outputs.pr_number }}
+          INPUT_PR_TITLE: ${{ steps.bridge.outputs.pr_title }}${{ steps.legacy.outputs.pr_title }}
+          INPUT_PR_URL: ${{ steps.bridge.outputs.pr_url }}${{ steps.legacy.outputs.pr_url }}
+          INPUT_EVENT_NAME: ${{ steps.bridge.outputs.event_name }}${{ steps.legacy.outputs.event_name }}
+          INPUT_MORD: ${{ steps.bridge.outputs.mOrD }}${{ steps.legacy.outputs.mOrD }}
+          INPUT_SOURCE: ${{ steps.bridge.outputs.pr_number != '' && 'bridge' || (steps.legacy.outputs.pr_number != '' && 'legacy' || 'none') }}
+          INPUT_COMMENT: ${{ steps.bridge.outputs.comment }}${{ steps.legacy.outputs.comment }}
         run: |
           {
-            echo "author=${{ steps.bridge.outputs.author }}${{ steps.legacy.outputs.author }}"
-            echo "pr_author=${{ steps.bridge.outputs.pr_author }}${{ steps.legacy.outputs.pr_author }}"
-            echo "pr_number=${{ steps.bridge.outputs.pr_number }}${{ steps.legacy.outputs.pr_number }}"
-            echo "pr_title=${{ steps.bridge.outputs.pr_title }}${{ steps.legacy.outputs.pr_title }}"
-            echo "pr_url=${{ steps.bridge.outputs.pr_url }}${{ steps.legacy.outputs.pr_url }}"
-            echo "event_name=${{ steps.bridge.outputs.event_name }}${{ steps.legacy.outputs.event_name }}"
-            echo "mOrD=${{ steps.bridge.outputs.mOrD }}${{ steps.legacy.outputs.mOrD }}"
-            echo "input_source=${{ steps.bridge.outputs.pr_number != '' && 'bridge' || (steps.legacy.outputs.pr_number != '' && 'legacy' || 'none') }}"
+            echo "author=${INPUT_AUTHOR}"
+            echo "pr_author=${INPUT_PR_AUTHOR}"
+            echo "pr_number=${INPUT_PR_NUMBER}"
+            echo "pr_title=${INPUT_PR_TITLE}"
+            echo "pr_url=${INPUT_PR_URL}"
+            echo "event_name=${INPUT_EVENT_NAME}"
+            echo "mOrD=${INPUT_MORD}"
+            echo "input_source=${INPUT_SOURCE}"
           } | tee -a "$GITHUB_OUTPUT"
-          printf 'comment<<EOF\n%s\nEOF\n' "${{ steps.bridge.outputs.comment }}${{ steps.legacy.outputs.comment }}" | tee -a "$GITHUB_OUTPUT"
+          printf 'comment<<EOF\n%s\nEOF\n' "${INPUT_COMMENT}" | tee -a "$GITHUB_OUTPUT"
 
       - name: Note legacy artifact fallback
         if: ${{ steps.inputs.outputs.input_source == 'legacy' }}
@@ -139,7 +149,7 @@ jobs:
           then
             legacy_suffix=" (legacy)"
           fi
-          metadata=$'trigger_name: ['"${trigger_name}"$']('"${trigger_run_url}"$')\nwf_run: [workflow_run]('"${wf_run_url}"$')'"${legacy_suffix}"
+          metadata=$'['"${trigger_name}"$']('"${trigger_run_url}"$'), [wf_run]('"${wf_run_url}"$')'"${legacy_suffix}"
           message="${message}"$'\n\n---\n'"${metadata}"
           printf 'title<<EOF\n%s\nEOF' "${message}" | tee "$GITHUB_OUTPUT"
         env:
@@ -153,6 +163,7 @@ jobs:
 
       - name: Send message on Zulip
         if: ${{ steps.actorTeams.outputs.isTeamMember == 'true' }}
+        continue-on-error: true
         uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
         with:
           api-key: ${{ secrets.ZULIP_API_KEY }}
@@ -176,12 +187,13 @@ jobs:
           then
             legacy_suffix=" (legacy)"
           fi
-          metadata=$'trigger_name: ['"${trigger_name}"$']('"${trigger_run_url}"$')\nwf_run: [workflow_run]('"${wf_run_url}"$')'"${legacy_suffix}"
+          metadata=$'['"${trigger_name}"$']('"${trigger_run_url}"$'), [wf_run]('"${wf_run_url}"$')'"${legacy_suffix}"
           body="${body}"$'\n\n---\n'"${metadata}"
           printf 'body<<EOF\n%s\nEOF\n' "${body}" | tee -a "$GITHUB_OUTPUT"
 
       - name: Add comment to PR
         if: ${{ steps.actorTeams.outputs.isTeamMember == 'true' }}
+        continue-on-error: true
         uses: GrantBirki/comment@608e41b19bc973020ec0e189ebfdae935d7fe0cc # v2.1.1
         with:
           # if a comment triggers the action, then `issue.number` is set
@@ -202,6 +214,7 @@ jobs:
 
       - name: Add label to PR
         if: ${{ steps.actorTeams.outputs.isTeamMember == 'true' }}
+        continue-on-error: true
         uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8.0.0
         with:
           # labels added by GITHUB_TOKEN won't trigger the Zulip emoji workflow

.github/workflows/zulip_emoji_ci_status.yaml

@@ -98,6 +98,7 @@ jobs:
 
     - name: Update CI emoji
       if: steps.pr.outputs.skip != 'true' && steps.action.outputs.ci_action != 'skip'
+      continue-on-error: true
       env:
         ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
         ZULIP_EMAIL: github-mathlib4-bot@leanprover.zulipchat.com

.github/workflows/zulip_emoji_closed_pr.yaml

@@ -61,6 +61,7 @@ jobs:
       - name: Update zulip emoji reactions
         if: ${{ ! startsWith(github.event.pull_request.title, '[Merged by Bors]') ||
                 github.event_name == 'reopened' }}
+        continue-on-error: true
         env:
           ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
           ZULIP_EMAIL: github-mathlib4-bot@leanprover.zulipchat.com

.github/workflows/zulip_emoji_labelling.yaml

@@ -37,6 +37,7 @@ jobs:
         pip install -r "$CI_SCRIPTS_DIR/zulip/requirements.txt"
 
     - name: Add or remove emoji
+      continue-on-error: true  # Emoji updates are cosmetic; never fail CI over them
       env:
         ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
         ZULIP_EMAIL: github-mathlib4-bot@leanprover.zulipchat.com

.github/workflows/zulip_emoji_merge_delegate.yaml

@@ -40,6 +40,7 @@ jobs:
         pip install -r "$CI_SCRIPTS_DIR/zulip/requirements.txt"
 
     - name: Update zulip emoji reactions
+      continue-on-error: true  # Emoji updates are cosmetic; never fail CI over them
       env:
         ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
         ZULIP_EMAIL: github-mathlib4-bot@leanprover.zulipchat.com

Archive/Imo/Imo1988Q6.lean

@@ -128,7 +128,7 @@ theorem constant_descent_vieta_jumping (x y : ℕ) {claim : Prop} {H : ℕ → 
   -- Let m be the smallest element of the nonempty set S.
   let m : ℕ := WellFounded.min Nat.lt_wfRel.wf S S_nonempty
   have m_mem : m ∈ S := WellFounded.min_mem Nat.lt_wfRel.wf S S_nonempty
-  have m_min : ∀ k ∈ S, ¬k < m := fun k hk => WellFounded.not_lt_min Nat.lt_wfRel.wf S S_nonempty hk
+  have m_min : ∀ k ∈ S, ¬k < m := fun k hk => WellFounded.not_lt_min Nat.lt_wfRel.wf S hk
   -- It suffices to show that there is point (a,b) with b ∈ S and b < m.
   rsuffices ⟨p', p'_mem, p'_small⟩ : ∃ p' : ℕ × ℕ, p'.2 ∈ S ∧ p'.2 < m
   · solve_by_elim

Cache/IO.lean

@@ -81,7 +81,7 @@ def CURLBIN :=
 
 /-- leantar version at https://github.com/digama0/leangz -/
 def LEANTARVERSION :=
-  "0.1.16"
+  "0.1.17"
 
 def EXE := if System.Platform.isWindows then ".exe" else ""
 

Counterexamples/AharoniKorman.lean

@@ -892,7 +892,7 @@ lemma x0y0_min (z : ℕ × ℕ) (hC : IsChain (· ≤ ·) C) (h : embed (n + 1)
   have : (C ∩ level (n + 1)).Nonempty := ⟨_, h, by simp [level_eq_range]⟩
   refine hC.le_of_not_gt h (x0y0_mem this) ?_
   rw [x0y0, dif_pos this, OrderEmbedding.lt_iff_lt]
-  exact wellFounded_lt.not_lt_min {x | embed (n + 1) x ∈ C} ?_ h
+  exact wellFounded_lt.not_lt_min {x | embed (n + 1) x ∈ C} h
 
 /--
 Given a subset `C` of the Hollom partial order, and an index `n`, find the smallest element of