Update lean-toolchain for leanprover/lean4#14259

Author: leanprover-community-mathlib4-bot

.git-blame-ignore-revs

@@ -0,0 +1,6 @@
+# 2024-05-20 replace `refine'` with one underscore by `refine` (#13059)
+7493b5f81b4c031b87877c5c124bea1ddc4e567d
+# 2024-05-24 replace many `refine'` with `refine` (#13166)
+fc48848e4374f13c796a7399bfccd2e228f776df
+# 2025-11-19 move Mathlib to the module system (#31786)
+6a54a80825b060ab20dc31751ebdce78b3a3b518

.github/actions/get-mathlib-ci/action.yml

@@ -10,7 +10,7 @@ inputs:
     # Default pinned commit used by workflows unless they explicitly override.
     # Update this ref as needed to pick up changes to mathlib-ci scripts
     # This is also updated automatically by .github/workflows/update_dependencies.yml
-    default: 5aee9d4ce5a39050c72b4aa46015a824b0c189ac
+    default: 0cd6cbc879d9241f3b4f6cb7e8291e34128c5654
   path:
     description: Checkout destination path.
     required: false

.github/workflows/PR_summary.yml

@@ -233,6 +233,16 @@ jobs:
         echo "Compute technical debt changes"
         techDebtVar="$("${CI_SCRIPTS_DIR}/reporting/technical-debt-metrics.sh" pr_summary)"
 
+        # If the PR decreased technical debt, add the `tech debt` label.
+        # The metrics script emits a summary line "Decrease in <level> tech debt:" for each
+        # level (strong/weak) that went down (and "Increase ..."/"No changes ..." otherwise),
+        # so matching either of those two lines means the PR reduced some tech debt.
+        if grep -qE "Decrease in (strong|weak) tech debt" <<< "${techDebtVar}"
+        then
+          printf $'Adding "tech debt" label to PR %s\n' "${PR}"
+          gh pr edit "${PR}" --add-label "tech debt"
+        fi
+
         echo "Compute documentation reminder"
         workflowFilesChanged="$(grep '^\.github/workflows/' changed_files.txt || true)"
         if [ -n "${workflowFilesChanged}" ]

.github/workflows/build_template.yml

@@ -801,6 +801,9 @@ jobs:
         run: |
           lake env lean scripts/create_deprecated_modules.lean
           lake env lean scripts/autolabel.lean
+          # Executing this also runs the export and writes a (gitignored) `crossrefs.json`,
+          # which doubles as a smoke test of the `export_crossrefs.yml` workflow.
+          lake env lean scripts/export_crossrefs.lean
           lake exe check_title_labels --labels "t-algebra" "feat: dummy PR for testing"
 
       - name: build everything

.github/workflows/export_crossrefs.yml

@@ -0,0 +1,161 @@
+name: Export cross-reference data
+
+# Generates a JSON dictionary of every declaration tagged with `@[wikidata]`,
+# `@[stacks]`, or `@[kerodon]` (name, file, line, and the referenced ids) and
+# pushes it to a versioned repository (`CROSSREFS_REPO`), where it is publicly
+# available at `https://raw.githubusercontent.com/<CROSSREFS_REPO>/master/crossrefs.json`.
+#
+# The data is read from the fully-imported `Mathlib` environment by
+# `scripts/export_crossrefs.lean`, like the `#stacks_tags` command.
+
+on:
+  workflow_run:
+    workflows: ["continuous integration"]
+    branches: [master]
+    types: [completed]
+  workflow_dispatch:
+    inputs:
+      dry_run:
+        description: "Dry run: mint the app token and verify push permission, but don't push to the crossrefs repo"
+        type: boolean
+        default: true
+
+concurrency:
+  group: export-crossrefs
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+  # Required for the token-minting action to request a GitHub OIDC token,
+  # which it exchanges (via Azure Key Vault) for a GitHub App installation token.
+  id-token: write
+
+env:
+  CROSSREFS_REPO: leanprover-community/crossref-exports
+  BUILT_SHA: ${{ github.event.workflow_run.head_sha || github.sha }}
+
+jobs:
+  export:
+    name: Export cross-reference JSON
+    runs-on: ubuntu-latest
+    environment:
+      name: crossref-exports
+      deployment: false
+    if: >-
+      github.repository == 'leanprover-community/mathlib4' &&
+      (github.event_name == 'workflow_dispatch'
+      || github.event.workflow_run.conclusion == 'success')
+    steps:
+      - name: Checkout the built commit
+        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+        with:
+          persist-credentials: false
+          # The exact commit CI validated; for manual runs, the dispatched ref.
+          ref: ${{ env.BUILT_SHA }}
+
+      - name: Configure Lean and fetch the Mathlib cache
+        uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0
+        with:
+          auto-config: false
+          use-github-cache: false
+          use-mathlib-cache: true
+          reinstall-transient-toolchain: true
+
+      - name: Generate crossrefs.json
+        env:
+          CROSSREFS_OUT: crossrefs.json
+          CROSSREFS_COMMIT: ${{ env.BUILT_SHA }}
+        run: lake env lean scripts/export_crossrefs.lean
+
+      - name: Sanity-check the output
+        run: |
+          jq -e '.entries | length > 0' crossrefs.json > /dev/null
+          echo "Exported $(jq '.entries | length' crossrefs.json) entries."
+
+      # Split `owner/repo` so the token can be scoped to the crossrefs repo. The
+      # app is installed on the crossrefs repo's owner, not on this repository,
+      # so the token-minting action must resolve the installation from there.
+      - name: Resolve crossrefs repository owner and name
+        id: repo
+        run: |
+          echo "owner=${CROSSREFS_REPO%%/*}" >> "$GITHUB_OUTPUT"
+          echo "name=${CROSSREFS_REPO#*/}" >> "$GITHUB_OUTPUT"
+
+      # Mint a short-lived GitHub App installation token scoped to the crossrefs
+      # repo, instead of relying on a long-lived personal access token.
+      - name: Generate app token
+        id: app-token
+        uses: leanprover-community/mathlib-ci/.github/actions/azure-create-github-app-token@3bb576208589a435eeaeac9b144a1b7c3e948760
+        with:
+          app-id: ${{ secrets.MATHLIB_CROSSREFS_APP_ID }}
+          key-vault-name: ${{ vars.MATHLIB_AZ_KEY_VAULT_NAME }}
+          key-name: crossref-exports-app-pk
+          azure-client-id: ${{ vars.GH_APP_AZURE_CLIENT_ID_CROSSREFS }}
+          azure-tenant-id: ${{ secrets.LPC_AZ_TENANT_ID }}
+          owner: ${{ steps.repo.outputs.owner }}
+          repositories: ${{ steps.repo.outputs.name }}
+
+      - name: Push to the crossrefs repository
+        env:
+          CROSSREFS_PUSH_TOKEN: ${{ steps.app-token.outputs.token }}
+          # On manual runs this defaults to true (see the workflow_dispatch
+          # inputs); on the automatic workflow_run trigger `inputs` is empty, so
+          # this is false and the push happens for real.
+          DRY_RUN: ${{ inputs.dry_run || false }}
+        run: |
+          git clone --depth 1 \
+            "https://x-access-token:${CROSSREFS_PUSH_TOKEN}@github.com/${CROSSREFS_REPO}.git" \
+            crossrefs-repo
+          cd crossrefs-repo
+          git config user.name  "leanprover-community-bot"
+          git config user.email "leanprover-community-bot@users.noreply.github.com"
+          # Commit only when the entries themselves change. The `generated`
+          # timestamp and source `commit` change on every run, so comparing the
+          # whole file would produce a commit even when nothing of substance did.
+          # Consequence: the published `generated`/`commit` fields record when the
+          # entries last changed, not the latest commit the export ran against, so
+          # consumers should not read `generated` as a "data freshness" signal.
+          # Read each file fully into a string and compare; using `diff -q` on two
+          # `jq` process substitutions makes `diff` close the pipes at the first
+          # difference, which leaves the `jq` writers with a SIGPIPE ("broken pipe")
+          # and noisy spurious errors in the log.
+          if [ -f crossrefs.json ] && \
+             [ "$(jq -Sc '.entries' crossrefs.json)" = "$(jq -Sc '.entries' ../crossrefs.json)" ]; then
+            echo "No change in entries."
+            changed=false
+          else
+            cp ../crossrefs.json crossrefs.json
+            git add crossrefs.json
+            git commit -m "Update crossrefs (mathlib4@${BUILT_SHA})"
+            changed=true
+          fi
+
+          if [ "${DRY_RUN}" = "true" ]; then
+            # Verify the minted token can actually push, without mutating the
+            # remote: `git push --dry-run` performs the authenticated
+            # git-receive-pack handshake (which GitHub gates on write access) but
+            # never sends the update. If nothing changed, add a throwaway local
+            # commit so there is a ref update to negotiate.
+            if [ "${changed}" != "true" ]; then
+              git commit --allow-empty -m "Dry-run push permission check (never sent)"
+            fi
+            echo "Dry run: verifying push permission against ${CROSSREFS_REPO} without pushing."
+            git push --dry-run
+          elif [ "${changed}" = "true" ]; then
+            git push
+          else
+            echo "No change in entries; nothing to commit."
+          fi
+
+      - name: Post failure message on Zulip
+        if: failure()
+        uses: zulip/github-actions-zulip/send-message@bd8ec52de371d139ae8313661b7d8318c19266aa # v2.0.1
+        with:
+          api-key: ${{ secrets.ZULIP_API_KEY }}
+          email: 'github-mathlib4-bot@leanprover.zulipchat.com'
+          organization-url: 'https://leanprover.zulipchat.com'
+          to: 'nightly-testing-mathlib'
+          type: 'stream'
+          topic: 'crossrefs export failure'
+          content: |
+            ❌ Cross-reference export [failed](${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}) on ${{ env.BUILT_SHA }}

.gitignore

@@ -10,3 +10,6 @@
 scripts/.rm_set_option_progress.jsonl
 # Artifacts from using the devcontainer setup
 .devcontainer/devcontainer-lock.json
+
+# Output of scripts/export_crossrefs.lean
+/crossrefs.json

Archive/Hairer.lean

@@ -93,6 +93,7 @@ def L : MvPolynomial ι ℝ →ₗ[ℝ]
     (fun p f₁ f₂ ↦ by simp_rw [smul_eq_mul, ← integral_add (int p _) (int p _), ← mul_add]; rfl)
     fun r p f ↦ by simp_rw [← integral_smul, smul_comm r]; rfl
 
+set_option backward.isDefEq.respectTransparency.types false in
 lemma inj_L : Injective (L ι) :=
   (injective_iff_map_eq_zero _).mpr fun p hp ↦ by
     have H : ∀ᵐ x : EuclideanSpace ℝ ι, x ∈ ball 0 1 → eval x p = 0 :=

Archive/Imo/Imo1987Q1.lean

@@ -31,6 +31,7 @@ open Finset (range sum_const)
 
 namespace Imo1987Q1
 
+set_option backward.isDefEq.respectTransparency false in
 /-- The set of pairs `(x : α, σ : Perm α)` such that `σ x = x` is equivalent to the set of pairs
 `(x : α, σ : Perm {x}ᶜ)`. -/
 def fixedPointsEquiv : { σx : α × Perm α // σx.2 σx.1 = σx.1 } ≃ Σ x : α, Perm ({x}ᶜ : Set α) :=
@@ -41,6 +42,7 @@ def fixedPointsEquiv : { σx : α × Perm α // σx.2 σx.1 = σx.1 } ≃ Σ x :
       (sigmaCongrRight fun x => Equiv.setCongr <| by simp only [SetCoe.forall]; simp)
     _ ≃ Σ x : α, Perm ({x}ᶜ : Set α) := sigmaCongrRight fun x => by apply Equiv.Set.compl
 
+set_option backward.isDefEq.respectTransparency false in
 theorem card_fixed_points :
     card { σx : α × Perm α // σx.2 σx.1 = σx.1 } = card α * (card α - 1)! := by
   simp only [card_congr (fixedPointsEquiv α), card_sigma, card_perm]

Archive/Imo/Imo1998Q2.lean

@@ -13,6 +13,7 @@ import Mathlib.Tactic.Ring
 
 /-!
 # IMO 1998 Q2
+
 In a competition, there are `a` contestants and `b` judges, where `b ≥ 3` is an odd integer. Each
 judge rates each contestant as either "pass" or "fail". Suppose `k` is a number such that, for any
 two judges, their ratings coincide for at most `k` contestants. Prove that `k / a ≥ (b - 1) / (2b)`.

Archive/Imo/Imo2001Q6.lean

@@ -9,6 +9,7 @@ import Mathlib.Tactic.LinearCombination
 
 /-!
 # IMO 2001 Q6
+
 Let $a$, $b$, $c$, $d$ be integers with $a > b > c > d > 0$. Suppose that
 
 $$ a*c + b*d = (a + b - c + d) * (-a + b + c + d). $$