Trigger CI for leanprover/lean4#6123

.github/workflows/discover-lean-pr-testing.yml

@@ -24,6 +24,23 @@ jobs:
         git config --global user.name "github-actions"
         git config --global user.email "github-actions@github.com"
 
+    - name: Determine old and new lean-toolchain
+      id: determine-toolchains
+      run: |
+        # `lean-toolchain` contains a string of the form "leanprover/lean4:nightly-2024-11-20"
+        # We grab the part after the ":"
+        NEW=$(cut -f2 -d: lean-toolchain)
+
+        # Find the commit hash of the previous change to `lean-toolchain`
+        PREV_COMMIT=$(git log -2 --format=format:%H -- lean-toolchain | tail -1)
+
+        # Get the contents of `lean-toolchain` from the previous commit
+        # The "./" in front of the path is important for `git show`
+        OLD=$(git show "$PREV_COMMIT":./lean-toolchain | cut -f2 -d:)
+
+        echo "new=$NEW" >> "$GITHUB_OUTPUT"
+        echo "old=$OLD" >> "$GITHUB_OUTPUT"
+
     - name: Clone lean4 repository and get PRs
       id: get-prs
       run: |
@@ -38,14 +55,15 @@ jobs:
         # Navigate to the cloned repository
         cd lean4-nightly || exit 1
 
-        # Shallow fetch of the last two tags
-        LAST_TWO_TAGS=$(git ls-remote --tags | grep nightly | tail -2 | cut -f2)
-        OLD=$(echo "$LAST_TWO_TAGS" | head -1)
-        NEW=$(echo "$LAST_TWO_TAGS" | tail -1)
+        # Use the OLD and NEW toolchains determined in the previous step
+        OLD="${{ steps.determine-toolchains.outputs.old }}"
+        NEW="${{ steps.determine-toolchains.outputs.new }}"
+
+        # Fetch the $OLD tag
         git fetch --depth=1 origin tag "$OLD" --no-tags
-        # Fetch the latest 100 commits prior to the $NEW tag.
-        # This should cover the terrain between $OLD and $NEW while still being a speedy download.
-        git fetch --depth=100 origin tag "$NEW" --no-tags
+        # Fetch the $NEW tag.
+        # This will only fetch commits newer than previously fetched commits (ie $OLD)
+        git fetch origin tag "$NEW" --no-tags
 
         PRS=$(git log --oneline "$OLD..$NEW" | sed 's/.*(#\([0-9]\+\))$/\1/')
         

.github/workflows/maintainer_bors.yml

@@ -19,13 +19,8 @@ jobs:
     # both set simultaneously: depending on the event that triggers the PR, usually only one is set
     env:
       AUTHOR: ${{ github.event.comment.user.login }}${{ github.event.review.user.login }}
-      PR_NUMBER: ${{ github.event.issue.number }}${{ github.event.pull_request.number }}
       COMMENT_EVENT: ${{ github.event.comment.body }}
       COMMENT_REVIEW: ${{ github.event.review.body }}
-      PR_TITLE_ISSUE: ${{ github.event.issue.title }}
-      PR_TITLE_PR: ${{ github.event.pull_request.title }}
-      PR_URL: ${{ github.event.issue.html_url }}${{ github.event.pull_request.html_url }}
-      EVENT_NAME: ${{ github.event_name }}
     name: Add ready-to-merge or delegated label
     runs-on: ubuntu-latest
     steps:
@@ -43,8 +38,7 @@ jobs:
 
           printf $'"bors delegate" or "bors merge" found? \'%s\'\n' "${m_or_d}"
           printf $'AUTHOR: \'%s\'\n' "${AUTHOR}"
-          printf $'PR_NUMBER: \'%s\'\n' "${PR_NUMBER}"
-          printf $'OTHER_NUMBER: \'%s\'\n' "${{ github.event.issue.number }}${{ github.event.pull_request.number }}"
+          printf $'PR_NUMBER: \'%s\'\n' "${{ github.event.issue.number }}${{ github.event.pull_request.number }}"
           printf $'%s' "${{ github.event.issue.number }}${{ github.event.pull_request.number }}" | hexdump -cC
 
           printf $'mOrD=%s\n' "${m_or_d}" >> "${GITHUB_OUTPUT}"
@@ -64,9 +58,6 @@ jobs:
         uses: actions-cool/check-user-permission@v2
         with:
           require: 'admin'
-          # review(_comment) use
-          # require: 'write'
-          # token: ${{ secrets.TRIAGE_TOKEN }}
 
       - name: Add ready-to-merge or delegated label
         id: add_label
@@ -75,13 +66,12 @@ jobs:
             steps.merge_or_delegate.outputs.bot == 'true' ) }}
         uses: octokit/request-action@v2.x
         with:
-          # check is this ok? was /repos/:repository/issues/:issue_number/labels
           route: POST /repos/:repository/issues/:issue_number/labels
           repository: ${{ github.repository }}
           issue_number: ${{ github.event.issue.number }}${{ github.event.pull_request.number }}
           labels: '["${{ steps.merge_or_delegate.outputs.mOrD }}"]'
         env:
-          GITHUB_TOKEN: ${{ secrets.TRIAGE_TOKEN }} # comment uses ${{ secrets.GITHUB_TOKEN }}
+          GITHUB_TOKEN: ${{ secrets.TRIAGE_TOKEN }}
 
       - if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' &&
           ( steps.user_permission.outputs.require-result == 'true' ||
@@ -92,6 +82,6 @@ jobs:
         # (and send an annoying email) if the labels don't exist
         run: |
           curl --request DELETE \
-            --url "https://api.github.com/repos/${{ github.repository }}/issues/${PR_NUMBER}/labels/awaiting-author" \
+            --url "https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}${{ github.event.pull_request.number }}/labels/awaiting-author" \
             --header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'
             # comment uses ${{ secrets.GITHUB_TOKEN }}

Archive/Imo/Imo2008Q2.lean

@@ -106,12 +106,7 @@ theorem imo2008_q2b : Set.Infinite rationalSolutions := by
             exact ⟨rfl, rfl, rfl⟩
         · have hg : -z = g (x, y, z) := rfl
           rw [hg, hz_def]; ring
-      have h₂ : q < t * (t + 1) := by
-        calc
-          q < q + 1 := by linarith
-          _ ≤ t := le_max_left (q + 1) 1
-          _ ≤ t + t ^ 2 := by linarith [sq_nonneg t]
-          _ = t * (t + 1) := by ring
+      have h₂ : q < t * (t + 1) := by linarith [sq_nonneg t, le_max_left (q + 1) 1]
       exact ⟨h₁, h₂⟩
     have hK_inf : Set.Infinite K := by intro h; apply hK_not_bdd; exact Set.Finite.bddAbove h
     exact hK_inf.of_image g

Archive/Imo/Imo2013Q5.lean

@@ -65,15 +65,9 @@ theorem le_of_all_pow_lt_succ' {x y : ℝ} (hx : 1 < x) (hy : 0 < y)
   refine le_of_all_pow_lt_succ hx ?_ h
   by_contra! hy'' : y ≤ 1
   -- Then there exists y' such that 0 < y ≤ 1 < y' < x.
-  let y' := (x + 1) / 2
-  have h_y'_lt_x : y' < x :=
-    calc
-      (x + 1) / 2 < x * 2 / 2 := by linarith
-      _ = x := by field_simp
-  have h1_lt_y' : 1 < y' :=
-    calc
-      1 = 1 * 2 / 2 := by field_simp
-      _ < (x + 1) / 2 := by linarith
+  have h_y'_lt_x : (x + 1) / 2 < x := by linarith
+  have h1_lt_y' : 1 < (x + 1) / 2 := by linarith
+  set y' := (x + 1) / 2
   have h_y_lt_y' : y < y' := by linarith
   have hh : ∀ n, 0 < n → x ^ n - 1 < y' ^ n := by
     intro n hn

Mathlib.lean

@@ -298,6 +298,9 @@ import Mathlib.Algebra.Group.Subgroup.Actions
 import Mathlib.Algebra.Group.Subgroup.Basic
 import Mathlib.Algebra.Group.Subgroup.Defs
 import Mathlib.Algebra.Group.Subgroup.Finite
+import Mathlib.Algebra.Group.Subgroup.Ker
+import Mathlib.Algebra.Group.Subgroup.Lattice
+import Mathlib.Algebra.Group.Subgroup.Map
 import Mathlib.Algebra.Group.Subgroup.MulOpposite
 import Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
 import Mathlib.Algebra.Group.Subgroup.Order

Mathlib/Algebra/AddConstMap/Basic.lean

@@ -28,6 +28,8 @@ We use parameters `a` and `b` instead of `1` to accommodate for two use cases:
   including orientation-reversing maps.
 -/
 
+assert_not_exists Finset
+
 open Function Set
 
 /-- A bundled map `f : G → H` such that `f (x + a) = f x + b` for all `x`.

Mathlib/Algebra/AddConstMap/Equiv.lean

@@ -5,6 +5,7 @@ Authors: Yury Kudryashov
 -/
 import Mathlib.Algebra.AddConstMap.Basic
 import Mathlib.GroupTheory.Perm.Basic
+
 /-!
 # Equivalences conjugating `(· + a)` to `(· + b)`
 
@@ -14,6 +15,8 @@ to be the type of equivalences such that `∀ x, f (x + a) = f x + b`.
 We also define the corresponding typeclass and prove some basic properties.
 -/
 
+assert_not_exists Finset
+
 open Function
 open scoped AddConstMap
 

Mathlib/Algebra/ContinuedFractions/Computation/Basic.lean

@@ -58,6 +58,7 @@ with a head term (`seq1`) is then transformed to a generalized continued fractio
 numerics, number theory, approximations, fractions
 -/
 
+assert_not_exists Finset
 
 namespace GenContFract
 

Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean

@@ -37,6 +37,7 @@ of three sections:
   parts.
 -/
 
+assert_not_exists Finset
 
 namespace GenContFract