-
Notifications
You must be signed in to change notification settings - Fork 367
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Trigger CI for leanprover/lean4#2695
- Loading branch information
Showing
5,568 changed files
with
647,473 additions
and
504,627 deletions.
The diff you're trying to view is too large. We only load the first 3000 changed files.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,4 @@ | ||
| self-hosted-runner: | ||
| labels: | ||
| - bors | ||
| - pr |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,85 @@ | ||
| name: Post PR summary comment | ||
|
|
||
| on: | ||
| pull_request: | ||
|
|
||
| jobs: | ||
| build: | ||
| runs-on: ubuntu-latest | ||
|
|
||
| steps: | ||
| - name: Checkout code | ||
| uses: actions/checkout@v4 | ||
| with: | ||
| fetch-depth: 0 | ||
|
|
||
| - name: Set up Python | ||
| uses: actions/setup-python@v5 | ||
| with: | ||
| python-version: 3.12 | ||
|
|
||
| - name: Install dependencies | ||
| run: | | ||
| python -m pip install --upgrade pip | ||
| sudo apt-get install -y jq | ||
| # If you have additional dependencies, install them here | ||
| - name: Get changed files | ||
| run: | | ||
| git fetch origin ${{ github.base_ref }} # fetch the base branch | ||
| git diff --name-only origin/${{ github.base_ref }}... > changed_files.txt # get the list of changed files | ||
| - name: Compute transitive imports | ||
| run: | | ||
| # the checkout dance, to avoid a detached head | ||
| git checkout master | ||
| git checkout - | ||
| currentHash="$(git rev-parse HEAD)" | ||
| # Compute the counts for the HEAD of the PR | ||
| python ./scripts/count-trans-deps.py "Mathlib/" > head.json | ||
| # Checkout the merge base | ||
| git checkout "$(git merge-base master ${{ github.sha }})" | ||
| # Compute the counts for the merge base | ||
| python ./scripts/count-trans-deps.py "Mathlib/" > base.json | ||
| # switch back to the current branch: the `declarations_diff` script should be here | ||
| git checkout "${currentHash}" | ||
| - name: Post or update the summary comment | ||
| env: | ||
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | ||
| BRANCH_NAME: ${{ github.head_ref }} | ||
| run: | | ||
| PR="${{ github.event.pull_request.number }}" | ||
| title="### PR summary" | ||
| ## Import count comment | ||
| importCount=$( | ||
| python ./scripts/import-graph-report.py base.json head.json changed_files.txt | ||
| ./scripts/import_trans_difference.sh | ||
| ) | ||
| if [ "$(printf '%s' "${importCount}" | wc -l)" -gt 12 ] | ||
| then | ||
| importCount="$(printf '<details><summary>\n\n%s\n\n</summary>\n\n%s\n\n</details>\n' "#### Import changes for modified files" "${importCount}")" | ||
| else | ||
| importCount="$(printf '#### Import changes for modified files\n\n%s\n' "${importCount}")" | ||
| fi | ||
| ## Declarations' diff comment | ||
| declDiff=$(./scripts/declarations_diff.sh) | ||
| if [ "$(printf '%s' "${declDiff}" | wc -l)" -gt 15 ] | ||
| then | ||
| declDiff="$(printf '<details><summary>\n\n%s\n\n</summary>\n\n%s\n\n</details>\n' "#### Declarations diff" "${declDiff}")" | ||
| else | ||
| declDiff="$(printf '#### Declarations diff\n\n%s\n' "${declDiff}")" | ||
| fi | ||
| git checkout "${BRANCH_NAME}" | ||
| currentHash="$(git rev-parse HEAD)" | ||
| hashURL="https://github.com/${{ github.repository }}/pull/${{ github.event.pull_request.number }}/commits/${currentHash}" | ||
| message="$(printf '%s [%s](%s)\n\n%s\n\n---\n\n%s\n' "${title}" "$(git rev-parse --short HEAD)" "${hashURL}" "${importCount}" "${declDiff}")" | ||
| ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,20 @@ | ||
| name: Actionlint | ||
| on: | ||
| push: | ||
| branches: | ||
| - 'master' | ||
| paths: | ||
| - '.github/**' | ||
| pull_request: | ||
| paths: | ||
| - '.github/**' | ||
| merge_group: | ||
|
|
||
| jobs: | ||
| actionlint: | ||
| runs-on: ubuntu-latest | ||
| steps: | ||
| - name: Checkout | ||
| uses: actions/checkout@v4 | ||
| - name: actionlint | ||
| uses: raven-actions/actionlint@v1 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.