Skip to content

Commit

Permalink
Trigger CI for leanprover/lean4#6123
Browse files Browse the repository at this point in the history
  • Loading branch information
leanprover-community-mathlib4-bot committed Nov 20, 2024
2 parents 11713e2 + 33e7503 commit 117f7f1
Show file tree
Hide file tree
Showing 512 changed files with 10,632 additions and 5,637 deletions.
6 changes: 5 additions & 1 deletion .github/build.in.yml
Original file line number Diff line number Diff line change
Expand Up @@ -156,6 +156,10 @@ jobs:
run: |
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
- name: print the sizes of the oleans
run: |
du .lake/build/lib/Mathlib || echo "This code should be unreachable"
- name: upload cache
# We only upload the cache if the build started (whether succeeding, failing, or cancelled)
# but not if any earlier step failed or was cancelled.
Expand Down Expand Up @@ -266,7 +270,7 @@ jobs:
with:
linters: gcc
run:
lake test
lake --iofail test

- name: check for unused imports
id: shake
Expand Down
6 changes: 5 additions & 1 deletion .github/workflows/bors.yml
Original file line number Diff line number Diff line change
Expand Up @@ -166,6 +166,10 @@ jobs:
run: |
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
- name: print the sizes of the oleans
run: |
du .lake/build/lib/Mathlib || echo "This code should be unreachable"
- name: upload cache
# We only upload the cache if the build started (whether succeeding, failing, or cancelled)
# but not if any earlier step failed or was cancelled.
Expand Down Expand Up @@ -276,7 +280,7 @@ jobs:
with:
linters: gcc
run:
lake test
lake --iofail test

- name: check for unused imports
id: shake
Expand Down
6 changes: 5 additions & 1 deletion .github/workflows/build.yml
Original file line number Diff line number Diff line change
Expand Up @@ -173,6 +173,10 @@ jobs:
run: |
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
- name: print the sizes of the oleans
run: |
du .lake/build/lib/Mathlib || echo "This code should be unreachable"
- name: upload cache
# We only upload the cache if the build started (whether succeeding, failing, or cancelled)
# but not if any earlier step failed or was cancelled.
Expand Down Expand Up @@ -283,7 +287,7 @@ jobs:
with:
linters: gcc
run:
lake test
lake --iofail test

- name: check for unused imports
id: shake
Expand Down
6 changes: 5 additions & 1 deletion .github/workflows/build_fork.yml
Original file line number Diff line number Diff line change
Expand Up @@ -170,6 +170,10 @@ jobs:
run: |
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
- name: print the sizes of the oleans
run: |
du .lake/build/lib/Mathlib || echo "This code should be unreachable"
- name: upload cache
# We only upload the cache if the build started (whether succeeding, failing, or cancelled)
# but not if any earlier step failed or was cancelled.
Expand Down Expand Up @@ -280,7 +284,7 @@ jobs:
with:
linters: gcc
run:
lake test
lake --iofail test

- name: check for unused imports
id: shake
Expand Down
33 changes: 15 additions & 18 deletions .github/workflows/discover-lean-pr-testing.yml
Original file line number Diff line number Diff line change
Expand Up @@ -24,34 +24,30 @@ jobs:
git config --global user.name "github-actions"
git config --global user.email "github-actions@github.com"
- name: Read date from lean-toolchain
id: fetch-date
run: |
TODAY=$(grep -oP 'nightly-\K\d{4}-\d{2}-\d{2}' lean-toolchain)
echo "TODAY=$TODAY" >> "$GITHUB_ENV"
- name: Set YESTERDAY
id: set-yesterday
run: |
YESTERDAY=$(date -d "$TODAY -1 day" +%Y-%m-%d)
echo "YESTERDAY=$YESTERDAY" >> "$GITHUB_ENV"
- name: Clone lean4-nightly repository and get PRs
- name: Clone lean4 repository and get PRs
id: get-prs
run: |
NIGHTLY_URL="https://github.com/leanprover/lean4-nightly.git"
# Create a temporary directory for cloning
cd "$(mktemp -d)" || exit 1
# Clone the repository with a depth of 30 (adjust as needed)
git clone --depth 30 "$NIGHTLY_URL"
# Clone the repository with a depth of 1
git clone --depth 1 "$NIGHTLY_URL"
# Navigate to the cloned repository
cd lean4-nightly || exit 1
YESTERDAY="${{ steps.set-yesterday.outputs.yesterday }}"
TODAY="${{ steps.fetch-date.outputs.today }}"
PRS=$(git log --oneline "nightly-$YESTERDAY..nightly-$TODAY" | sed 's/.*(#\([0-9]\+\))$/\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)
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
PRS=$(git log --oneline "$OLD..$NEW" | sed 's/.*(#\([0-9]\+\))$/\1/')
# Output the PRs
echo "$PRS"
Expand All @@ -64,6 +60,7 @@ jobs:
PRS="${{ steps.get-prs.outputs.prs }}"
echo "$PRS" | tr ' ' '\n' > prs.txt
MATCHING_BRANCHES=$(git branch -r | grep -f prs.txt)
echo "$MATCHING_BRANCHES"
# Initialize an empty variable to store branches with relevant diffs
RELEVANT_BRANCHES=""
Expand Down
97 changes: 97 additions & 0 deletions .github/workflows/maintainer_bors.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,97 @@
name: Add "ready-to-merge" and "delegated" label

# triggers the action when
on:
# the PR receives a comment
issue_comment:
types: [created]
# 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]

jobs:
add_ready_to_merge_label:
# 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: Add ready-to-merge or delegated label
runs-on: ubuntu-latest
steps:
- name: Find bors 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=^bors *\(merge\|r+\) *$=ready-to-merge=p; s=^bors *d.*=delegated=p' | head -1)"
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 $'%s' "${{ github.event.issue.number }}${{ github.event.pull_request.number }}" | hexdump -cC
printf $'mOrD=%s\n' "${m_or_d}" >> "${GITHUB_OUTPUT}"
if [ "${AUTHOR}" == 'leanprover-community-mathlib4-bot' ] ||
[ "${AUTHOR}" == 'leanprover-community-bot-assistant' ]
then
printf $'bot=true\n'
printf $'bot=true\n' >> "${GITHUB_OUTPUT}"
else
printf $'bot=false\n'
printf $'bot=false\n' >> "${GITHUB_OUTPUT}"
fi
- name: Check whether user is a mathlib admin
id: user_permission
if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' }}
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
if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' &&
( steps.user_permission.outputs.require-result == 'true' ||
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 }}

- if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' &&
( steps.user_permission.outputs.require-result == 'true' ||
steps.merge_or_delegate.outputs.bot == 'true' ) }}
id: remove_labels
name: Remove "awaiting-author"
# we use curl rather than octokit/request-action so that the job won't fail
# (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" \
--header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'
# comment uses ${{ secrets.GITHUB_TOKEN }}
3 changes: 2 additions & 1 deletion .github/workflows/maintainer_merge.yml
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,8 @@ jobs:
printf 'Comment:"%s"\n' "${COMMENT}"
m_or_d="$(printf '%s' "${COMMENT}" |
sed -n 's=^maintainer *\(merge\|delegate\) *$=\1=p' | head -1)"
# captures `maintainer merge/delegate` as well as an optional `?`, ignoring subsequent spaces
sed -n 's=^maintainer *\(merge\|delegate\)\(?\?\) *$=\1\2=p' | head -1)"
printf $'"maintainer delegate" or "maintainer merge" found? \'%s\'\n' "${m_or_d}"
Expand Down
7 changes: 7 additions & 0 deletions .github/workflows/update_dependencies.yml
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,13 @@ jobs:
# Only return if PR is still open
filterOutClosed: true

- name: Print PR, if found
run: echo "Found PR ${prNumber} at ${prUrl}"
if: steps.PR.outputs.pr_found == 'true'
env:
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: |
Expand Down
2 changes: 1 addition & 1 deletion Archive/Imo/Imo1998Q2.lean
Original file line number Diff line number Diff line change
Expand Up @@ -202,7 +202,7 @@ end

theorem clear_denominators {a b k : ℕ} (ha : 0 < a) (hb : 0 < b) :
(b - 1 : ℚ) / (2 * b) ≤ k / a ↔ ((b : ℕ) - 1) * a ≤ k * (2 * b) := by
rw [div_le_div_iff]
rw [div_le_div_iff]
-- Porting note: proof used to finish with `<;> norm_cast <;> simp [ha, hb]`
· convert Nat.cast_le (α := ℚ)
· aesop
Expand Down
2 changes: 1 addition & 1 deletion Archive/Imo/Imo2001Q2.lean
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ namespace Imo2001Q2

theorem bound (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
a ^ 4 / (a ^ 4 + b ^ 4 + c ^ 4) ≤ a ^ 3 / sqrt ((a ^ 3) ^ 2 + ↑8 * b ^ 3 * c ^ 3) := by
rw [div_le_div_iff (by positivity) (by positivity)]
rw [div_le_div_iff (by positivity) (by positivity)]
calc a ^ 4 * sqrt ((a ^ 3) ^ 2 + (8:ℝ) * b ^ 3 * c ^ 3)
= a ^ 3 * (a * sqrt ((a ^ 3) ^ 2 + (8:ℝ) * b ^ 3 * c ^ 3)) := by ring
_ ≤ a ^ 3 * (a ^ 4 + b ^ 4 + c ^ 4) := ?_
Expand Down
Loading

0 comments on commit 117f7f1

Please sign in to comment.