Skip to content

Commit 1dcc62e

Browse files
mattrobballmattrobball
committed
Merge branch 'master' into mrb/adic_completion
2 parents 4a75374 + 94099b4 commit 1dcc62e

248 files changed

Lines changed: 2915 additions & 2341 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/workflows/PR_summary.yml‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -99,6 +99,8 @@ jobs:
9999
## Technical debt changes
100100
techDebtVar="$(./scripts/technical-debt-metrics.sh pr_summary)"
101101
102-
message="$(printf '%s [%s](%s)%s\n\n%s\n\n---\n\n%s\n\n---\n\n%s\n' "${title}" "$(git rev-parse --short HEAD)" "${hashURL}" "${high_percentages}" "${importCount}" "${declDiff}" "${techDebtVar}")"
102+
# store in a file, to avoid "long arguments" error.
103+
printf '%s [%s](%s)%s\n\n%s\n\n---\n\n%s\n\n---\n\n%s\n' "${title}" "$(git rev-parse --short HEAD)" "${hashURL}" "${high_percentages}" "${importCount}" "${declDiff}" "${techDebtVar}" > messageFile.md
103104
104-
./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}"
105+
cat messageFile.md
106+
./scripts/update_PR_comment.sh messageFile.md "${title}" "${PR}"

‎.github/workflows/bot_fix_style.yaml‎

Lines changed: 164 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,164 @@
1+
name: bot fix style
2+
3+
# triggers the action when
4+
on:
5+
issue_comment:
6+
# the PR receives a comment, or a comment is edited
7+
types: [created, edited]
8+
pull_request_review:
9+
# triggers on a review, whether or not it is accompanied by a comment
10+
types: [submitted]
11+
pull_request_review_comment:
12+
# triggers on a review comment
13+
types: [created, edited]
14+
15+
jobs:
16+
fix_style:
17+
# we set some variables. The ones of the form `${{ X }}${{ Y }}` are typically not
18+
# both set simultaneously: depending on the event that triggers the PR, usually only one is set
19+
env:
20+
AUTHOR: ${{ github.event.comment.user.login }}${{ github.event.review.user.login }}
21+
COMMENT_EVENT: ${{ github.event.comment.body }}
22+
COMMENT_REVIEW: ${{ github.event.review.body }}
23+
COMMENT_REVIEW_COMMENT: ${{ github.event.pull_request_review_comment.body }}
24+
name: Fix style issues from lint
25+
# the `if` works with `comment`s, but not with `review`s or `review_comment`s
26+
# if: github.event.issue.pull_request
27+
# && (startsWith(github.event.comment.body, 'bot fix style') || contains(toJSON(github.event.comment.body), '\nbot fix style'))
28+
runs-on: ubuntu-latest
29+
steps:
30+
- name: Find bot fix style
31+
id: bot_fix_style
32+
run: |
33+
COMMENT="${COMMENT_EVENT}${COMMENT_REVIEW}${COMMENT_REVIEW_COMMENT}"
34+
# we strip `\r` since line endings from GitHub contain this character
35+
COMMENT="${COMMENT//$'\r'/}"
36+
# for debugging, we print some information
37+
printf '%s' "${COMMENT}" | hexdump -cC
38+
printf 'Comment:"%s"\n' "${COMMENT}"
39+
bot_fix_style="$(printf '%s' "${COMMENT}" |
40+
sed -n 's=^bot fix style$=bot-fix-style=p' | head -1)"
41+
42+
printf $'"bot fix style"? \'%s\'\n' "${bot_fix_style}"
43+
printf $'AUTHOR: \'%s\'\n' "${AUTHOR}"
44+
printf $'PR_NUMBER: \'%s\'\n' "${{ github.event.issue.number }}${{ github.event.pull_request.number }}"
45+
printf $'%s' "${{ github.event.issue.number }}${{ github.event.pull_request.number }}" | hexdump -cC
46+
47+
printf $'bot_fix_style=%s\n' "${bot_fix_style}" >> "${GITHUB_OUTPUT}"
48+
# these final variables are probably not relevant for the bot_fix_style action
49+
if [ "${AUTHOR}" == 'leanprover-community-mathlib4-bot' ] ||
50+
[ "${AUTHOR}" == 'leanprover-community-bot-assistant' ]
51+
then
52+
printf $'bot=true\n'
53+
printf $'bot=true\n' >> "${GITHUB_OUTPUT}"
54+
else
55+
printf $'bot=false\n'
56+
printf $'bot=false\n' >> "${GITHUB_OUTPUT}"
57+
fi
58+
59+
- id: user_permission
60+
if: steps.bot_fix_style.outputs.bot_fix_style == 'bot-fix-style'
61+
uses: actions-cool/check-user-permission@v2
62+
with:
63+
require: 'write'
64+
65+
# from now on, it is sufficient to just check `user_permission`:
66+
# if the comment did not contain `bot fix style`,
67+
# then `user_permission` would not have ran
68+
- name: Add reaction (comment)
69+
# reactions are only supported for `comment`s and `review_comment`s?
70+
# This action only runs on `comment`s rather than `review`s or `review_comment`s
71+
# Is the `id` check a good way to check that this is a `comment`?
72+
if: ${{ steps.user_permission.outputs.require-result == 'true' &&
73+
! github.event.comment.id == '' }}
74+
uses: peter-evans/create-or-update-comment@v4
75+
with:
76+
comment-id: ${{ github.event.comment.id }}
77+
reactions: rocket
78+
79+
- name: Add reaction (review comment)
80+
# this action only runs on `review_comment`s
81+
# is the `id` check a good way to check that this is a `review_comment`?
82+
if: ${{ steps.user_permission.outputs.require-result == 'true' &&
83+
! github.event.pull_request_review_comment.id == '' }}
84+
run: |
85+
gh api --method POST \
86+
-H "Accept: application/vnd.github+json" \
87+
-H "X-GitHub-Api-Version: 2022-11-28" \
88+
/repos/${{ github.repository_owner }}/${{ github.event.repository.name }}/pulls/comments/${{ github.event.comment.id }}/reactions \
89+
-f "content=rocket"
90+
env:
91+
GH_TOKEN: ${{ secrets.BOT_FIX_STYLE_TOKEN }}
92+
93+
- name: cleanup
94+
if: steps.user_permission.outputs.require-result == 'true'
95+
run: |
96+
find . -name . -o -prune -exec rm -rf -- {} +
97+
98+
- uses: actions/checkout@v4
99+
if: steps.user_permission.outputs.require-result == 'true'
100+
with:
101+
token: ${{ secrets.BOT_FIX_STYLE_TOKEN }}
102+
103+
- name: Checkout PR branch
104+
if: steps.user_permission.outputs.require-result == 'true'
105+
run: |
106+
# covers `comment`s
107+
gh pr checkout ${{ github.event.issue.number }} ||
108+
# covers `review`s and `review_comment`s
109+
gh pr checkout ${{ github.event.pull_request.number }}
110+
env:
111+
GH_TOKEN: ${{ secrets.BOT_FIX_STYLE_TOKEN }}
112+
113+
- name: install Python
114+
if: steps.user_permission.outputs.require-result == 'true'
115+
uses: actions/setup-python@v5
116+
with:
117+
python-version: 3.8
118+
119+
- name: install elan
120+
if: steps.user_permission.outputs.require-result == 'true'
121+
run: |
122+
set -o pipefail
123+
curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
124+
./elan-init -y --default-toolchain none
125+
echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
126+
127+
# run the same linting steps as in lint_and_suggest_pr.yaml
128+
129+
- name: lint
130+
if: steps.user_permission.outputs.require-result == 'true'
131+
run: |
132+
lake exe lint-style --fix
133+
134+
- name: Install bibtool
135+
if: steps.user_permission.outputs.require-result == 'true'
136+
run: |
137+
sudo apt-get update
138+
sudo apt-get install -y bibtool
139+
140+
- name: lint references.bib
141+
if: steps.user_permission.outputs.require-result == 'true'
142+
run: |
143+
# ignoring the return code allows the following `reviewdog` step to add GitHub suggestions
144+
./scripts/lint-bib.sh || true
145+
146+
- name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
147+
if: steps.user_permission.outputs.require-result == 'true'
148+
run: |
149+
# ignoring the return code allows the following `reviewdog` step to add GitHub suggestions
150+
lake exe mk_all || true
151+
152+
- name: Commit and push changes
153+
if: steps.user_permission.outputs.require-result == 'true'
154+
run: |
155+
# cleanup junk from build
156+
rm elan-init
157+
rm docs/references.bib.old
158+
# setup commit and push
159+
git config user.name "leanprover-community-mathlib4-bot"
160+
git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"
161+
git add .
162+
# Don't fail if there's nothing to commit
163+
git commit -m "commit changes from style linters" || true
164+
git push origin HEAD

‎.github/workflows/bot_fix_style_comment.yaml‎

Lines changed: 0 additions & 93 deletions
This file was deleted.

‎.github/workflows/bot_fix_style_review.yaml‎

Lines changed: 0 additions & 99 deletions
This file was deleted.

0 commit comments

Comments
 (0)