Trigger CI for leanprover-community/batteries#1034

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

@@ -12,10 +12,10 @@ jobs:
     runs-on: ubuntu-latest
 
     steps:
-    - name: Checkout mathlib repository
+    - name: Checkout mathlib4 repository
       uses: actions/checkout@v4
       with:
-        repository: leanprover-community/mathlib
+        repository: leanprover-community/mathlib4
         ref: nightly-testing
         fetch-depth: 0  # Fetch all branches
 

.github/workflows/maintainer_merge.yml

@@ -0,0 +1,113 @@
+name: Maintainer merge
+
+# triggers the action when
+on:
+  # the PR receives a comment
+  issue_comment:
+    types: [created, edited]
+  # the PR receives a review
+  pull_request_review:
+    # whether or not it is accompanied by a comment
+    types: [submitted]
+  # the PR receives a review comment
+  pull_request_review_comment:
+    types: [created, edited]
+
+jobs:
+  ping_zulip:
+    # we set some variables. The ones of the form `${{ X }}${{ Y }}` are typically not
+    # 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: Ping maintainers on Zulip
+    runs-on: ubuntu-latest
+    steps:
+      - name: Find maintainer merge/delegate
+        id: merge_or_delegate
+        run: |
+          COMMENT="${COMMENT_EVENT}${COMMENT_REVIEW}"
+          # we strip `\r` since line endings from GitHub contain this character
+          COMMENT="${COMMENT//$'\r'/}"
+          # for debugging, we print some information
+          printf '%s' "${COMMENT}" | hexdump -cC
+          printf 'Comment:"%s"\n' "${COMMENT}"
+          m_or_d="$(printf '%s' "${COMMENT}" |
+            sed -n 's=^maintainer  *\(merge\|delegate\)$=\1=p' | head -1)"
+
+          printf $'"maintainer delegate" or "maintainer merge" found? \'%s\'\n' "${m_or_d}"
+
+          printf $'mOrD=%s\n' "${m_or_d}" > "${GITHUB_OUTPUT}"
+
+      - name: Check whether user is part of mathlib-reviewers team
+        if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' }}
+        uses: TheModdingInquisition/actions-team-membership@v1.0
+        with:
+          organization: 'leanprover-community'
+          team: 'mathlib-reviewers' # required. The team to check for
+          token: ${{ secrets.MATHLIB_REVIEWERS_TEAM_KEY }} # required. Personal Access Token with the `read:org` permission
+          comment: 'You seem to not be authorized' # optional. A comment to post if the user is not part of the team.
+                                                   # This feature is only applicable in an issue (or PR) context
+          exit: true # optional. If the action should exit if the user is not part of the team. Defaults to true.
+
+      - name: Checkout
+        if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' }}
+        uses: actions/checkout@v4
+
+      - name: Determine Zulip topic
+        if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' }}
+        id: determine_topic
+        run: |
+          ./scripts/get_tlabel.sh "/repos/leanprover-community/mathlib4/issues/${PR_NUMBER}" >> "$GITHUB_OUTPUT"
+        env:
+          GH_TOKEN: ${{secrets.GITHUB_TOKEN}}
+
+      - name: Form the message
+        if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' }}
+        id: form_the_message
+        run: |
+          # for debugging, we print the available variables
+          echo "github.event.action: '${{ github.event.action }}'"
+
+          echo ""
+          message="$(
+            ./scripts/maintainer_merge_message.sh "${AUTHOR}" "${{ steps.merge_or_delegate.outputs.mOrD }}" "${EVENT_NAME}" "${PR_NUMBER}" "${PR_URL}" "${PR_TITLE_ISSUE}${PR_TITLE_PR}"
+          )"
+          printf 'title<<EOF\n%s\n[CI run](%s)\nEOF' "${message}" "https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}" | tee "$GITHUB_OUTPUT"
+
+      - name: Send message on Zulip
+        if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' }}
+        uses: zulip/github-actions-zulip/send-message@v1
+        with:
+          api-key: ${{ secrets.ZULIP_API_KEY }}
+          email: 'github-mathlib4-bot@leanprover.zulipchat.com'
+          organization-url: 'https://leanprover.zulipchat.com'
+          to: 'mathlib reviewers'
+          type: 'stream'
+          topic: ${{ steps.determine_topic.outputs.topic }}
+          content: ${{ steps.form_the_message.outputs.title }}
+
+      - name: Add comment to PR
+        if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' }}
+        uses: GrantBirki/comment@v2
+        with:
+          # if a comment triggers the action, then `issue.number` is set
+          # if a review or review comment triggers the action, then `pull_request.number` is set
+          issue-number: ${{ github.event.issue.number }}${{ github.event.pull_request.number }}
+          body: |
+            🚀 Pull request has been placed on the maintainer queue by ${{ github.event.comment.user.login }}${{ github.event.review.user.login }}.
+
+      - name: Add label to PR
+        if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' }}
+        uses: actions/github-script@v7
+        with:
+          github-token: ${{secrets.GITHUB_TOKEN}}
+          script: |
+            const { owner, repo, number: issue_number } = context.issue;
+            await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['maintainer-merge'] });

Archive/Imo/Imo1960Q1.lean

@@ -45,14 +45,14 @@ theorem ge_100 {n : ℕ} (h1 : ProblemPredicate n) : 100 ≤ n := by
     rw [← h1.left]
     refine Nat.base_pow_length_digits_le 10 n ?_ (not_zero h1)
     simp
-  linarith
+  omega
 
 theorem lt_1000 {n : ℕ} (h1 : ProblemPredicate n) : n < 1000 := by
   have h2 : n < 10 ^ 3 := by
     rw [← h1.left]
     refine Nat.lt_base_pow_length_digits ?_
     simp
-  linarith
+  omega
 
 /-
 We do an exhaustive search to show that all results are covered by `SolutionPredicate`.
@@ -70,7 +70,7 @@ theorem searchUpTo_step {c n} (H : SearchUpTo c n) {c' n'} (ec : c + 1 = c') (en
   refine ⟨by ring, fun m l p => ?_⟩
   obtain ⟨h₁, ⟨m, rfl⟩, h₂⟩ := id p
   by_cases h : 11 * m < c * 11; · exact H _ h p
-  obtain rfl : m = c := by linarith
+  obtain rfl : m = c := by omega
   rw [Nat.mul_div_cancel_left _ (by norm_num : 11 > 0), mul_comm] at h₂
   refine (H' h₂).imp ?_ ?_ <;> · rintro rfl; norm_num