Update lean-toolchain for leanprover/lean4#10524

Author: leanprover-community-mathlib4-bot

.github/build.in.yml

@@ -671,16 +671,6 @@ jobs:
           lint-bib-file: true
           ref: ${{ PR_BRANCH_REF }}
 
-  build_and_lint:
-    name: CI Success
-    if: FORK_CONDITION
-    needs: [style_lint, post_steps]
-    runs-on: ubuntu-latest
-    steps:
-      - name: succeed
-        run: |
-          echo "Success: Required build and lint checks completed!"
-
   final:
     name: Post-CI jobJOB_NAME
     if: FORK_CONDITION

.github/workflows/bors.yml

@@ -681,16 +681,6 @@ jobs:
           lint-bib-file: true
           ref: ${{ github.sha }}
 
-  build_and_lint:
-    name: CI Success
-    if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing'
-    needs: [style_lint, post_steps]
-    runs-on: ubuntu-latest
-    steps:
-      - name: succeed
-        run: |
-          echo "Success: Required build and lint checks completed!"
-
   final:
     name: Post-CI job
     if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing'

.github/workflows/build.yml

@@ -688,16 +688,6 @@ jobs:
           lint-bib-file: true
           ref: ${{ github.sha }}
 
-  build_and_lint:
-    name: CI Success
-    if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing'
-    needs: [style_lint, post_steps]
-    runs-on: ubuntu-latest
-    steps:
-      - name: succeed
-        run: |
-          echo "Success: Required build and lint checks completed!"
-
   final:
     name: Post-CI job
     if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing'

.github/workflows/build_fork.yml

@@ -685,16 +685,6 @@ jobs:
           lint-bib-file: true
           ref: ${{ github.event.pull_request.head.sha }}
 
-  build_and_lint:
-    name: CI Success
-    if: github.event.pull_request.head.repo.fork
-    needs: [style_lint, post_steps]
-    runs-on: ubuntu-latest
-    steps:
-      - name: succeed
-        run: |
-          echo "Success: Required build and lint checks completed!"
-
   final:
     name: Post-CI job (fork)
     if: github.event.pull_request.head.repo.fork

.github/workflows/label_new_contributor.yml

@@ -2,7 +2,10 @@ name: Label New Contributors
 
 # Written with ChatGPT: https://chat.openai.com/share/3777ceb1-d722-4705-bacd-ba3f04b387be
 
-on: pull_request_target
+on: 
+  pull_request_target:
+    types:
+      - opened
 
 # Limit permissions for GITHUB_TOKEN for the entire workflow
 permissions:
@@ -36,6 +39,10 @@ jobs:
             const issues = await github.paginate(opts)
             const pullRequestCount = issues.length;
 
+            // We could filter out bot users here, with:
+            // const isBot = (github.rest.users.getByUsername(creator).type === "Bot");
+            // But we choose to label PRs by new bot contributors as well.
+
             // Determine if the creator has 5 or fewer pull requests
             if (pullRequestCount <= 5) {
               // Add the "new-contributor" label to the current pull request

.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

.github/workflows/nolints.yml

@@ -11,27 +11,7 @@ jobs:
     runs-on: ubuntu-latest
     if: github.repository == 'leanprover-community/mathlib4'
     steps:
-      - name: cleanup
-        run: |
-          find . -name . -o -prune -exec rm -rf -- {} +
-
-      # The Hoskinson runners may not have jq installed, so do that now.
-      - name: 'Setup jq'
-        uses: dcarbone/install-jq-action@f0e10f46ff84f4d32178b4b76e1ef180b16f82c3 # v3.1.1
-
       - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
-        with:
-          ## fetch the whole repository, as we want to push to it later
-          fetch-depth: 0
-
-      - name: prune ProofWidgets .lake
-        run: |
-          # The ProofWidgets release contains not just the `.js` (which we need in order to build)
-          # but also `.oleans`, which may have been built with the wrong toolchain.
-          # This removes them.
-          # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nightly-testing/near/411225235
-          rm -rf .lake/packages/proofwidgets/.lake/build/lib
-          rm -rf .lake/packages/proofwidgets/.lake/build/ir
 
       - name: Configure Lean
         uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # 2025-04-24
@@ -40,31 +20,22 @@ jobs:
           use-github-cache: false
           use-mathlib-cache: true
 
-      - name: build mathlib
-        id: build
-        uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
-        with:
-          linters: lean
-          run: |
-            bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
-
       - name: update nolints.json
         shell: bash
         run: |
           env LEAN_ABORT_ON_PANIC=1 lake exe runLinter --update Mathlib
 
-      - name: configure git setup
-        run: |
-          git remote add origin-bot "https://leanprover-community-bot:${{ secrets.UPDATE_NOLINTS_TOKEN }}@github.com/leanprover-community/mathlib4.git"
-          git config user.email "[email protected]"
-          git config user.name "leanprover-community-bot"
-
-          # By default, github actions overrides the credentials used to access any
-          # github url so that it uses the github-actions[bot] user.  We want to access
-          # github using a different username.
-          git config --unset http.https://github.com/.extraheader
-
-      - name: file a new PR to update nolints.json
-        run: ./scripts/update_nolints_CI.sh
-        env:
-          DEPLOY_GITHUB_TOKEN: ${{ secrets.UPDATE_NOLINTS_TOKEN }}
+      - name: Create Pull Request
+        uses: peter-evans/create-pull-request@271a8d0340265f705b14b6d32b9829c1cb33d45e # v7.0.8
+        with:
+          token: "${{ secrets.UPDATE_NOLINTS_TOKEN }}"
+          author: "leanprover-community-bot <[email protected]>"
+          commit-message: "chore(scripts): update nolints.json"
+          branch: "nolints"
+          base: master
+          title: "chore(scripts): update nolints.json"
+          body: |
+            I am happy to remove some nolints for you!
+
+            [workflow run for this PR](${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }})
+          labels: "auto-merge-after-CI"

.github/workflows/update_dependencies.yml

@@ -9,6 +9,8 @@ jobs:
   update-dependencies:
     runs-on: ubuntu-latest
     if: github.repository == 'leanprover-community/mathlib4'
+    env:
+      BRANCH_NAME: "update-dependencies-bot-use-only"
     steps:
       - name: Checkout repository
         uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
@@ -23,13 +25,28 @@ jobs:
           use-github-cache: false
           use-mathlib-cache: false
 
+      - name: Get branch SHA if it exists
+        id: get-branch-sha
+        run: |
+          # Check if the branch exists remotely
+          if git fetch origin "$BRANCH_NAME"; then
+            SHA=$(git rev-parse "origin/$BRANCH_NAME")
+            echo "Branch '$BRANCH_NAME' exists with SHA: $SHA"
+            echo "sha=$SHA" >> "${GITHUB_OUTPUT}"
+          else
+            echo "Branch '$BRANCH_NAME' does not exist"
+            echo "sha=" >>" ${GITHUB_OUTPUT}"
+          fi
+
       - name: Get PR and labels
+        if: ${{ steps.get-branch-sha.outputs.sha != '' }}
         id: PR # all the steps below are skipped if 'ready-to-merge' is in the list of labels found here
         uses: 8BitJonny/gh-get-current-pr@4056877062a1f3b624d5d4c2bedefa9cf51435c9 # 4.0.0
         # TODO: this may not work properly if the same commit is pushed to multiple branches:
         # https://github.com/8BitJonny/gh-get-current-pr/issues/8
         with:
           github-token: ${{ secrets.GITHUB_TOKEN }}
+          sha: ${{ steps.get-branch-sha.outputs.sha }}
           # Only return if PR is still open
           filterOutClosed: true
 
@@ -40,12 +57,6 @@ jobs:
           prNumber: ${{ steps.PR.outputs.number }}
           prUrl: ${{ steps.PR.outputs.pr_url }}
 
-      - name: Configure Git User
-        if: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') }}
-        run: |
-          git config user.name "leanprover-community-mathlib4-bot"
-          git config user.email "[email protected]"
-
       - name: Update dependencies
         if: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') }}
         run: lake update -v
@@ -61,22 +72,44 @@ jobs:
             echo "toolchain_modified=false" >> "$GITHUB_OUTPUT"
           fi
 
-      - name: Generate PR title
+      - name: Check if lake-manifest.json was modified
         if: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') && steps.check_toolchain.outputs.toolchain_modified != 'true' }}
+        id: check_manifest
+        run: |
+          if [ -n "${{ steps.get-branch-sha.outputs.sha }}" ]; then
+            # Branch exists, compare the file
+            if git diff --quiet HEAD "origin/$BRANCH_NAME" -- lake-manifest.json; then
+              echo "has_diff=false" >> "${GITHUB_OUTPUT}"
+              echo "No differences in lake-manifest.json"
+            else
+              echo "has_diff=true" >> "${GITHUB_OUTPUT}"
+              echo "Differences found in lake-manifest.json"
+            fi
+          else
+            # Branch doesn't exist, consider it as different
+            echo "has_diff=true" >> "${GITHUB_OUTPUT}"
+            echo "Branch does not exist, treating as different"
+          fi
+
+      - name: Generate PR title
+        if: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') && steps.check_manifest.outputs.has_diff == 'true' }}
         run: |
           echo "timestamp=$(date -u +"%Y-%m-%d-%H-%M")" >> "$GITHUB_ENV"
           echo "pr_title=chore: update Mathlib dependencies $(date -u +"%Y-%m-%d")" >> "$GITHUB_ENV"
 
       - name: Create Pull Request
-        if: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') && steps.check_toolchain.outputs.toolchain_modified != 'true' }}
+        if: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') && steps.check_manifest.outputs.has_diff == 'true' }}
         uses: peter-evans/create-pull-request@271a8d0340265f705b14b6d32b9829c1cb33d45e # v7.0.8
         with:
           token: "${{ secrets.UPDATE_DEPENDENCIES_TOKEN }}"
           author: "leanprover-community-mathlib4-bot <[email protected]>"
           commit-message: "chore: update Mathlib dependencies ${{ env.timestamp }}"
           # this branch is referenced in update_dependencies_zulip.yml
-          branch: "update-dependencies-bot-use-only"
+          branch: ${{ env.BRANCH_NAME }}
           base: master
           title: "${{ env.pr_title }}"
-          body: "This PR updates the Mathlib dependencies."
+          body: |
+            This PR updates the Mathlib dependencies.
+
+            [workflow run for this PR](${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }})
           labels: "auto-merge-after-CI"

Archive/Arithcc.lean

@@ -209,13 +209,13 @@ protected theorem StateEq.refl (t : Register) (ζ : State) : ζ ≃[t] ζ := by
 
 @[symm]
 protected theorem StateEq.symm {t : Register} (ζ₁ ζ₂ : State) : ζ₁ ≃[t] ζ₂ → ζ₂ ≃[t] ζ₁ := by
-  simp [StateEq]; intros
+  simp only [StateEq, and_imp]; intros
   constructor <;> (symm; assumption)
 
 @[trans]
 protected theorem StateEq.trans {t : Register} (ζ₁ ζ₂ ζ₃ : State) :
     ζ₁ ≃[t] ζ₂ → ζ₂ ≃[t] ζ₃ → ζ₁ ≃[t] ζ₃ := by
-  simp [StateEq]; intros
+  simp only [StateEq, and_imp]; intros
   constructor
   · simp_all only
   · trans ζ₂ <;> assumption
@@ -227,7 +227,7 @@ instance (t : Register) : Trans (StateEq (t + 1)) (StateEq (t + 1)) (StateEq (t
 @[trans]
 protected theorem StateEqStateEqRs.trans (t : Register) (ζ₁ ζ₂ ζ₃ : State) :
     ζ₁ ≃[t] ζ₂ → ζ₂ ≃[t]/ac ζ₃ → ζ₁ ≃[t]/ac ζ₃ := by
-  simp [StateEq]; intros
+  simp only [StateEq, and_imp]; intros
   trans ζ₂ <;> assumption
 
 instance (t : Register) : Trans (StateEq (t + 1)) (StateEqRs (t + 1)) (StateEqRs (t + 1)) :=
@@ -236,7 +236,7 @@ instance (t : Register) : Trans (StateEq (t + 1)) (StateEqRs (t + 1)) (StateEqRs
 /-- Writing the same value to register `t` gives `≃[t + 1]` from `≃[t]`. -/
 theorem stateEq_implies_write_eq {t : Register} {ζ₁ ζ₂ : State} (h : ζ₁ ≃[t] ζ₂) (v : Word) :
     write t v ζ₁ ≃[t + 1] write t v ζ₂ := by
-  simp [StateEq, StateEqRs] at *
+  simp only [StateEq, StateEqRs, write] at *
   constructor; · exact h.1
   intro r hr
   have hr : r ≤ t := Register.le_of_lt_succ hr
@@ -249,15 +249,15 @@ theorem stateEq_implies_write_eq {t : Register} {ζ₁ ζ₂ : State} (h : ζ₁
 /-- Writing the same value to any register preserves `≃[t]/ac`. -/
 theorem stateEqRs_implies_write_eq_rs {t : Register} {ζ₁ ζ₂ : State} (h : ζ₁ ≃[t]/ac ζ₂)
     (r : Register) (v : Word) : write r v ζ₁ ≃[t]/ac write r v ζ₂ := by
-  simp [StateEqRs] at *
+  simp only [StateEqRs, write] at *
   intro r' hr'
   specialize h r' hr'
   congr
 
 /-- `≃[t + 1]` with writing to register `t` implies `≃[t]`. -/
 theorem write_eq_implies_stateEq {t : Register} {v : Word} {ζ₁ ζ₂ : State}
     (h : ζ₁ ≃[t + 1] write t v ζ₂) : ζ₁ ≃[t] ζ₂ := by
-  simp [StateEq, StateEqRs] at *
+  simp only [StateEq, write, StateEqRs] at *
   constructor; · exact h.1
   intro r hr
   obtain ⟨_, h⟩ := h
@@ -313,10 +313,10 @@ theorem compiler_correctness
     have hζ₃ : ζ₃ ≃[t + 1] { write t ν₁ η with ac := ν₂ } := calc
       ζ₃ = outcome (compile map e_s₂ (t + 1)) ζ₂ := by simp_all
       _ ≃[t + 1] { ζ₂ with ac := ν₂ } := by apply e_ih_s₂ <;> assumption
-      _ ≃[t + 1] { write t ν₁ η with ac := ν₂ } := by simp [StateEq]; apply hζ₂
+      _ ≃[t + 1] { write t ν₁ η with ac := ν₂ } := by simpa [StateEq]
     have hζ₃_ν₂ : ζ₃.ac = ν₂ := by simp_all [StateEq]
     have hζ₃_ν₁ : read t ζ₃ = ν₁ := by
-      simp [StateEq, StateEqRs] at hζ₃ ⊢
+      simp only [StateEq, StateEqRs, write, read] at hζ₃ ⊢
       obtain ⟨_, hζ₃⟩ := hζ₃
       specialize hζ₃ t (Register.lt_succ_self _)
       simp_all

Archive/Imo/Imo2008Q2.lean

@@ -46,8 +46,8 @@ theorem imo2008_q2a (x y z : ℝ) (h : x * y * z = 1) (hx : x ≠ 1) (hy : y ≠
     x ^ 2 / (x - 1) ^ 2 + y ^ 2 / (y - 1) ^ 2 + z ^ 2 / (z - 1) ^ 2 ≥ 1 := by
   obtain ⟨a, b, c, ha, hb, hc, rfl, rfl, rfl⟩ := subst_abc h
   obtain ⟨m, n, rfl, rfl⟩ : ∃ m n, b = c - m ∧ a = c - m - n := by use c - b, b - a; simp
-  have hm_ne_zero : m ≠ 0 := by contrapose! hy; simp [field]; assumption
-  have hn_ne_zero : n ≠ 0 := by contrapose! hx; simp [field]; assumption
+  have hm_ne_zero : m ≠ 0 := by contrapose! hy; simpa [field]
+  have hn_ne_zero : n ≠ 0 := by contrapose! hx; simpa [field]
   have hmn_ne_zero : m + n ≠ 0 := by contrapose! hz; field_simp; linarith
   have hc_sub_sub : c - (c - m - n) = m + n := by abel
   rw [ge_iff_le, ← sub_nonneg]