From 73a6ac92544e76747949ce7f88343c821b79e568 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 09:21:07 +0200 Subject: [PATCH 001/191] add find_labels --- .github/workflows/lint_and_suggest_pr.yml | 5 +++++ scripts/find_labels.sh | 25 +++++++++++++++++++++++ 2 files changed, 30 insertions(+) create mode 100755 scripts/find_labels.sh diff --git a/.github/workflows/lint_and_suggest_pr.yml b/.github/workflows/lint_and_suggest_pr.yml index 64f06540402cd3..0dd369e21bbf60 100644 --- a/.github/workflows/lint_and_suggest_pr.yml +++ b/.github/workflows/lint_and_suggest_pr.yml @@ -28,6 +28,11 @@ jobs: ./elan-init -y --default-toolchain none echo "$HOME/.elan/bin" >> "${GITHUB_PATH}" + - name: report + continue-on-error: true + run: | + ./scripts/find_labels.sh leanprover-community mathlib4 + - name: lint continue-on-error: true # allows the following `reviewdog` step to add GitHub suggestions run: | diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh new file mode 100755 index 00000000000000..d0797e17ab79f5 --- /dev/null +++ b/scripts/find_labels.sh @@ -0,0 +1,25 @@ +#!/bin/bash + +# Check if required arguments are provided +if [ "$#" -ne 2 ]; then + echo "Usage: $0 " + exit 1 +fi + +repo_owner=$1 +repo_name=$2 + +# Get the date for one month ago +one_month_ago=$(date -d '1 month ago' +%Y-%m-%d) + +# Retrieve merged PRs from the last month +prs=$(gh pr list --repo "$repo_owner/$repo_name" --state merged --search "merged:>$one_month_ago" --json number,labels) + +# Check if any PRs are found +if [ -z "$prs" ]; then + echo "No merged pull requests found from the last month." + exit 0 +fi + +# Print PR numbers and their labels +echo "$prs" | jq -r '.[] | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels")"' From 713a1b71f52cd26450931f56c5903bb15abf61e5 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 09:23:48 +0200 Subject: [PATCH 002/191] excl --- scripts/find_labels.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index d0797e17ab79f5..8c74b877fe490e 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -17,7 +17,7 @@ prs=$(gh pr list --repo "$repo_owner/$repo_name" --state merged --search "merged # Check if any PRs are found if [ -z "$prs" ]; then - echo "No merged pull requests found from the last month." + echo "No merged pull requests found from the last month!" exit 0 fi From 9d491b694e24e791079481f7a1edbe0fa9266457 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 09:27:05 +0200 Subject: [PATCH 003/191] token? --- .github/workflows/lint_and_suggest_pr.yml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/.github/workflows/lint_and_suggest_pr.yml b/.github/workflows/lint_and_suggest_pr.yml index 0dd369e21bbf60..955ce6fdff641f 100644 --- a/.github/workflows/lint_and_suggest_pr.yml +++ b/.github/workflows/lint_and_suggest_pr.yml @@ -5,6 +5,10 @@ on: name: lint and suggest jobs: + + env: + GH_TOKEN: ${{ github.token }} + style_lint: if: github.repository == 'leanprover-community/mathlib4' && github.event.pull_request.draft == false name: Lint style From 557f339e6cc6cbf62044def26cbdcaf15cc9cff4 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 09:28:15 +0200 Subject: [PATCH 004/191] format message --- scripts/declarations_diff.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/scripts/declarations_diff.sh b/scripts/declarations_diff.sh index bde0906978c26e..d12f8de3182fa1 100755 --- a/scripts/declarations_diff.sh +++ b/scripts/declarations_diff.sh @@ -165,6 +165,7 @@ printf $'
./scripts/declarations_diff.sh long ```
+ The doc-module for `script/declarations_diff.sh` contains some details about this script.' : < Date: Wed, 31 Jul 2024 09:29:13 +0200 Subject: [PATCH 005/191] move env --- .github/workflows/lint_and_suggest_pr.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/lint_and_suggest_pr.yml b/.github/workflows/lint_and_suggest_pr.yml index 955ce6fdff641f..f2e1c805bc6e3b 100644 --- a/.github/workflows/lint_and_suggest_pr.yml +++ b/.github/workflows/lint_and_suggest_pr.yml @@ -6,9 +6,6 @@ name: lint and suggest jobs: - env: - GH_TOKEN: ${{ github.token }} - style_lint: if: github.repository == 'leanprover-community/mathlib4' && github.event.pull_request.draft == false name: Lint style @@ -32,6 +29,9 @@ jobs: ./elan-init -y --default-toolchain none echo "$HOME/.elan/bin" >> "${GITHUB_PATH}" + env: + GH_TOKEN: ${{ github.token }} + - name: report continue-on-error: true run: | From f1c4c5a1afacdf29bc64311f5577b090c4870258 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 09:30:37 +0200 Subject: [PATCH 006/191] move env --- .github/workflows/lint_and_suggest_pr.yml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/.github/workflows/lint_and_suggest_pr.yml b/.github/workflows/lint_and_suggest_pr.yml index f2e1c805bc6e3b..f8c0f119c25239 100644 --- a/.github/workflows/lint_and_suggest_pr.yml +++ b/.github/workflows/lint_and_suggest_pr.yml @@ -10,6 +10,10 @@ jobs: if: github.repository == 'leanprover-community/mathlib4' && github.event.pull_request.draft == false name: Lint style runs-on: ubuntu-latest + + env: + GH_TOKEN: ${{ github.token }} + steps: - name: cleanup run: | @@ -29,9 +33,6 @@ jobs: ./elan-init -y --default-toolchain none echo "$HOME/.elan/bin" >> "${GITHUB_PATH}" - env: - GH_TOKEN: ${{ github.token }} - - name: report continue-on-error: true run: | From c9af61b4a0a6eea59d0f5ee8989995595683d971 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 09:41:50 +0200 Subject: [PATCH 007/191] checkout master --- scripts/find_labels.sh | 2 ++ 1 file changed, 2 insertions(+) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 8c74b877fe490e..39eae6bdfca86e 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -12,6 +12,8 @@ repo_name=$2 # Get the date for one month ago one_month_ago=$(date -d '1 month ago' +%Y-%m-%d) +git checkout master + # Retrieve merged PRs from the last month prs=$(gh pr list --repo "$repo_owner/$repo_name" --state merged --search "merged:>$one_month_ago" --json number,labels) From 3d7de1783df3cc23d16047c5b432f47ecea26904 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 09:45:10 +0200 Subject: [PATCH 008/191] origin --- scripts/find_labels.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 39eae6bdfca86e..cd5ee879637480 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -12,7 +12,7 @@ repo_name=$2 # Get the date for one month ago one_month_ago=$(date -d '1 month ago' +%Y-%m-%d) -git checkout master +git checkout origin/master # Retrieve merged PRs from the last month prs=$(gh pr list --repo "$repo_owner/$repo_name" --state merged --search "merged:>$one_month_ago" --json number,labels) From f5dd7fe8c9ca066bb5b832bca7ae314c45f4527b Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 09:45:53 +0200 Subject: [PATCH 009/191] closed, rather than merged --- scripts/find_labels.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index cd5ee879637480..0fc42d54581a60 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -15,7 +15,7 @@ one_month_ago=$(date -d '1 month ago' +%Y-%m-%d) git checkout origin/master # Retrieve merged PRs from the last month -prs=$(gh pr list --repo "$repo_owner/$repo_name" --state merged --search "merged:>$one_month_ago" --json number,labels) +prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "closed:>$one_month_ago" --json number,labels) # Check if any PRs are found if [ -z "$prs" ]; then From a8e65ae93e6a0e5323332d3fb02f5f50ff07b5e5 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 09:46:37 +0200 Subject: [PATCH 010/191] switch --- scripts/find_labels.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 0fc42d54581a60..8482b019b72a71 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -12,7 +12,7 @@ repo_name=$2 # Get the date for one month ago one_month_ago=$(date -d '1 month ago' +%Y-%m-%d) -git checkout origin/master +git switch origin/master # Retrieve merged PRs from the last month prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "closed:>$one_month_ago" --json number,labels) From 39e0a4492ea83623110f8396558fc55e51da08e8 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 09:50:49 +0200 Subject: [PATCH 011/191] print date --- scripts/find_labels.sh | 2 ++ 1 file changed, 2 insertions(+) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 8482b019b72a71..1c4d27f29e0c0d 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -12,6 +12,8 @@ repo_name=$2 # Get the date for one month ago one_month_ago=$(date -d '1 month ago' +%Y-%m-%d) +printf 'Dates after %s\n' "${one_month_ago}" + git switch origin/master # Retrieve merged PRs from the last month From 8139287f1df23e054262979adb6141a4d2076706 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 09:54:16 +0200 Subject: [PATCH 012/191] fetch all --- .github/workflows/lint_and_suggest_pr.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/lint_and_suggest_pr.yml b/.github/workflows/lint_and_suggest_pr.yml index f8c0f119c25239..800f360d22819c 100644 --- a/.github/workflows/lint_and_suggest_pr.yml +++ b/.github/workflows/lint_and_suggest_pr.yml @@ -20,6 +20,8 @@ jobs: find . -name . -o -prune -exec rm -rf -- {} + - uses: actions/checkout@v4 + with: + fetch-depth: 0 - name: install Python uses: actions/setup-python@v4 From d6d231ce49d6693371919d8a141c38bdeb1a78d8 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 09:56:57 +0200 Subject: [PATCH 013/191] checkout later --- .github/workflows/lint_and_suggest_pr.yml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/lint_and_suggest_pr.yml b/.github/workflows/lint_and_suggest_pr.yml index 800f360d22819c..a2693850a3d07b 100644 --- a/.github/workflows/lint_and_suggest_pr.yml +++ b/.github/workflows/lint_and_suggest_pr.yml @@ -19,10 +19,6 @@ jobs: run: | find . -name . -o -prune -exec rm -rf -- {} + - - uses: actions/checkout@v4 - with: - fetch-depth: 0 - - name: install Python uses: actions/setup-python@v4 with: @@ -35,6 +31,10 @@ jobs: ./elan-init -y --default-toolchain none echo "$HOME/.elan/bin" >> "${GITHUB_PATH}" + - uses: actions/checkout@v4 + with: + fetch-depth: 0 + - name: report continue-on-error: true run: | From ad543165e7b58cb393da5c4e3c9f21c35ce1b06e Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 09:57:44 +0200 Subject: [PATCH 014/191] no origin --- scripts/find_labels.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 1c4d27f29e0c0d..8c5f374a1e4b9a 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -14,7 +14,7 @@ one_month_ago=$(date -d '1 month ago' +%Y-%m-%d) printf 'Dates after %s\n' "${one_month_ago}" -git switch origin/master +git switch master # Retrieve merged PRs from the last month prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "closed:>$one_month_ago" --json number,labels) From 23795f9e923ca9d94ea1da631786786edca1c931 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 10:04:46 +0200 Subject: [PATCH 015/191] do not filter much --- scripts/find_labels.sh | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 8c5f374a1e4b9a..7444c0c27b8920 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -17,7 +17,9 @@ printf 'Dates after %s\n' "${one_month_ago}" git switch master # Retrieve merged PRs from the last month -prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "closed:>$one_month_ago" --json number,labels) +prs=$(gh pr list --repo "$repo_owner/$repo_name" --json number,labels) + +# --state closed --search "closed:>$one_month_ago" # Check if any PRs are found if [ -z "$prs" ]; then From 70b9390461258ae9ab362101ebfd27a687102322 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 10:10:41 +0200 Subject: [PATCH 016/191] print more --- scripts/find_labels.sh | 24 ++++++++++++++---------- 1 file changed, 14 insertions(+), 10 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 7444c0c27b8920..dd9bf4f2d9ff1f 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -16,16 +16,20 @@ printf 'Dates after %s\n' "${one_month_ago}" git switch master -# Retrieve merged PRs from the last month -prs=$(gh pr list --repo "$repo_owner/$repo_name" --json number,labels) +page=1 +per_page=100 -# --state closed --search "closed:>$one_month_ago" +while :; do + # Retrieve merged PRs from the last month, paginated + prs=$(gh pr list --repo "$repo_owner/$repo_name" --state merged --search "merged:>$one_month_ago" --json number,labels --limit "$per_page" --page "$page") -# Check if any PRs are found -if [ -z "$prs" ]; then - echo "No merged pull requests found from the last month!" - exit 0 -fi + # Check if any PRs are found + if [ -z "$prs" ] || [ "$prs" = "[]" ]; then + break + fi + + # Print PR numbers and their labels + echo "$prs" | jq -r '.[] | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels")"' -# Print PR numbers and their labels -echo "$prs" | jq -r '.[] | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels")"' + page=$((page + 1)) +done From 65d04a39f4659902ee2a6bcd3cfb0e722920f326 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 10:13:36 +0200 Subject: [PATCH 017/191] no pages --- scripts/find_labels.sh | 23 ++++++++--------------- 1 file changed, 8 insertions(+), 15 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index dd9bf4f2d9ff1f..f16536899b8f31 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -16,20 +16,13 @@ printf 'Dates after %s\n' "${one_month_ago}" git switch master -page=1 -per_page=100 +# Retrieve merged PRs from the last month, paginated +prs=$(gh pr list --repo "$repo_owner/$repo_name" --state merged --search "merged:>$one_month_ago" --json number,labels --limit 100) -while :; do - # Retrieve merged PRs from the last month, paginated - prs=$(gh pr list --repo "$repo_owner/$repo_name" --state merged --search "merged:>$one_month_ago" --json number,labels --limit "$per_page" --page "$page") - - # Check if any PRs are found - if [ -z "$prs" ] || [ "$prs" = "[]" ]; then - break - fi - - # Print PR numbers and their labels - echo "$prs" | jq -r '.[] | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels")"' +# Check if any PRs are found +if [ -z "$prs" ] || [ "$prs" = "[]" ]; then + break +fi - page=$((page + 1)) -done +# Print PR numbers and their labels +echo "$prs" | jq -r '.[] | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels")"' From c6b67fa71ea8621383879d60639e08ddc8eed54a Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 10:15:19 +0200 Subject: [PATCH 018/191] closed --- scripts/find_labels.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index f16536899b8f31..6fdeab2ef34116 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -17,7 +17,7 @@ printf 'Dates after %s\n' "${one_month_ago}" git switch master # Retrieve merged PRs from the last month, paginated -prs=$(gh pr list --repo "$repo_owner/$repo_name" --state merged --search "merged:>$one_month_ago" --json number,labels --limit 100) +prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "closed:>$one_month_ago" --json number,labels --limit 100) # Check if any PRs are found if [ -z "$prs" ] || [ "$prs" = "[]" ]; then From 70857d09b6d645cb6f1ac59c091bea4b863c4d2b Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 10:20:11 +0200 Subject: [PATCH 019/191] used commit numbers as limit --- scripts/find_labels.sh | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 6fdeab2ef34116..e1dc1ee78746bc 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -16,8 +16,11 @@ printf 'Dates after %s\n' "${one_month_ago}" git switch master +# find how many commits to master there have been in the last month +last_month_commits="$(git log --since="$one_month_ago" --pretty=oneline | wc -l)" + # Retrieve merged PRs from the last month, paginated -prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "closed:>$one_month_ago" --json number,labels --limit 100) +prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "closed:>$one_month_ago" --json number,labels --limit "$last_month_commits") # Check if any PRs are found if [ -z "$prs" ] || [ "$prs" = "[]" ]; then From fb27aa98417ff6399997143fdf7505a2badf827b Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 10:36:42 +0200 Subject: [PATCH 020/191] print title --- scripts/find_labels.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index e1dc1ee78746bc..025170e8ec6578 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -20,7 +20,7 @@ git switch master last_month_commits="$(git log --since="$one_month_ago" --pretty=oneline | wc -l)" # Retrieve merged PRs from the last month, paginated -prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "closed:>$one_month_ago" --json number,labels --limit "$last_month_commits") +prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "closed:>$one_month_ago" --json number,labels,title --limit "$last_month_commits") # Check if any PRs are found if [ -z "$prs" ] || [ "$prs" = "[]" ]; then From ff57b09c2f5b0832d11b2fd3b6c641c639273fe2 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 10:39:53 +0200 Subject: [PATCH 021/191] print title really --- scripts/find_labels.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 025170e8ec6578..0636cefdf6420a 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -28,4 +28,4 @@ if [ -z "$prs" ] || [ "$prs" = "[]" ]; then fi # Print PR numbers and their labels -echo "$prs" | jq -r '.[] | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels")"' +echo "$prs" | jq -r '.[] | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Title: \(.title)"' From 09aa9498224acdc2f36801526c245ffae3681bbb Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 10:51:12 +0200 Subject: [PATCH 022/191] add number of commits --- scripts/find_labels.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 0636cefdf6420a..259b9e7f5bf514 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -12,13 +12,13 @@ repo_name=$2 # Get the date for one month ago one_month_ago=$(date -d '1 month ago' +%Y-%m-%d) -printf 'Dates after %s\n' "${one_month_ago}" - git switch master # find how many commits to master there have been in the last month last_month_commits="$(git log --since="$one_month_ago" --pretty=oneline | wc -l)" +printf '%s commits since %s\n' "${last_month_commits}" "${one_month_ago}" + # Retrieve merged PRs from the last month, paginated prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "closed:>$one_month_ago" --json number,labels,title --limit "$last_month_commits") From 2310592ccd56ff542eaa8a62a08ab001a5105daf Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 11:00:02 +0200 Subject: [PATCH 023/191] rename CI step --- .github/workflows/lint_and_suggest_pr.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/lint_and_suggest_pr.yml b/.github/workflows/lint_and_suggest_pr.yml index a2693850a3d07b..1e2f0d6fc8812a 100644 --- a/.github/workflows/lint_and_suggest_pr.yml +++ b/.github/workflows/lint_and_suggest_pr.yml @@ -35,7 +35,7 @@ jobs: with: fetch-depth: 0 - - name: report + - name: blog report continue-on-error: true run: | ./scripts/find_labels.sh leanprover-community mathlib4 From 6f191db98e6eda6ae07f9b049d24c4d52a15ed20 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 11:11:49 +0200 Subject: [PATCH 024/191] starts with `Merged by Bors` --- scripts/find_labels.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 259b9e7f5bf514..890930142e3014 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -28,4 +28,4 @@ if [ -z "$prs" ] || [ "$prs" = "[]" ]; then fi # Print PR numbers and their labels -echo "$prs" | jq -r '.[] | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Title: \(.title)"' +echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Title: \(.title)"' From d59268aa6c3c3efe59c40caaf4f640dbd0ba6d79 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 11:14:43 +0200 Subject: [PATCH 025/191] double the number of commits searched --- scripts/find_labels.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 890930142e3014..17772c8edb68f5 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -20,7 +20,7 @@ last_month_commits="$(git log --since="$one_month_ago" --pretty=oneline | wc -l) printf '%s commits since %s\n' "${last_month_commits}" "${one_month_ago}" # Retrieve merged PRs from the last month, paginated -prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "closed:>$one_month_ago" --json number,labels,title --limit "$last_month_commits") +prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "closed:>$one_month_ago" --json number,labels,title --limit "$((last_month_commits * 2))") # Check if any PRs are found if [ -z "$prs" ] || [ "$prs" = "[]" ]; then From 7fde707c0e2a27843143b55e3daefb7f274a448f Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 11:27:54 +0200 Subject: [PATCH 026/191] one fewer day --- scripts/find_labels.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 17772c8edb68f5..9aeae26353fd35 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -10,7 +10,7 @@ repo_owner=$1 repo_name=$2 # Get the date for one month ago -one_month_ago=$(date -d '1 month ago' +%Y-%m-%d) +one_month_ago=$(date -d '1 month ago - 1 day' +%Y-%m-%d) git switch master From 3bffc81f29fc51585bbe4737d9423f01843339e4 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 11:35:41 +0200 Subject: [PATCH 027/191] two different dates --- scripts/find_labels.sh | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 9aeae26353fd35..c9347f59721f27 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -10,13 +10,15 @@ repo_owner=$1 repo_name=$2 # Get the date for one month ago -one_month_ago=$(date -d '1 month ago - 1 day' +%Y-%m-%d) +one_month_ago=$(date -d '1 month ago' +%Y-%m-%d) git switch master # find how many commits to master there have been in the last month last_month_commits="$(git log --since="$one_month_ago" --pretty=oneline | wc -l)" +one_month_ago=$(date -d '1 month ago - 1 day' +%Y-%m-%d) + printf '%s commits since %s\n' "${last_month_commits}" "${one_month_ago}" # Retrieve merged PRs from the last month, paginated From 97a76bdb7d8e7f5a8da690fa56a5dc7398988eb2 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 11:38:31 +0200 Subject: [PATCH 028/191] print all prs --- scripts/find_labels.sh | 2 ++ 1 file changed, 2 insertions(+) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index c9347f59721f27..a40538d6220dab 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -29,5 +29,7 @@ if [ -z "$prs" ] || [ "$prs" = "[]" ]; then break fi +echo "${prs}" + # Print PR numbers and their labels echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Title: \(.title)"' From 2006ef2378e60479e30acec0ca8ff62497867322 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 11:53:03 +0200 Subject: [PATCH 029/191] do not print prs --- scripts/find_labels.sh | 2 -- 1 file changed, 2 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index a40538d6220dab..c9347f59721f27 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -29,7 +29,5 @@ if [ -z "$prs" ] || [ "$prs" = "[]" ]; then break fi -echo "${prs}" - # Print PR numbers and their labels echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Title: \(.title)"' From 5d291342453bd89e93f70d32cee04e38e3cb198b Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 12:22:39 +0200 Subject: [PATCH 030/191] 15 days --- scripts/find_labels.sh | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index c9347f59721f27..64a3192e90c19d 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -11,18 +11,20 @@ repo_name=$2 # Get the date for one month ago one_month_ago=$(date -d '1 month ago' +%Y-%m-%d) +one_month_ago=$(date -d '15 days ago' +%Y-%m-%d) git switch master # find how many commits to master there have been in the last month last_month_commits="$(git log --since="$one_month_ago" --pretty=oneline | wc -l)" -one_month_ago=$(date -d '1 month ago - 1 day' +%Y-%m-%d) +start_date=$(date -d '15 days ago - 1 day' +%Y-%m-%d) +end_date=$(date -d 'today' +%Y-%m-%d) -printf '%s commits since %s\n' "${last_month_commits}" "${one_month_ago}" +printf '%s commits between %s and %s\n' "${start_date}" "${end_date}" # Retrieve merged PRs from the last month, paginated -prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "closed:>$one_month_ago" --json number,labels,title --limit "$((last_month_commits * 2))") +prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "closed:>$start_date closed:<$end_date" --json number,labels,title --limit "$((last_month_commits * 2))") # Check if any PRs are found if [ -z "$prs" ] || [ "$prs" = "[]" ]; then From 75f13fc01a07ecbad4be9ecf076bcb7df6f92573 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 12:24:31 +0200 Subject: [PATCH 031/191] number of commits --- scripts/find_labels.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 64a3192e90c19d..9177c0dab46df3 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -21,7 +21,7 @@ last_month_commits="$(git log --since="$one_month_ago" --pretty=oneline | wc -l) start_date=$(date -d '15 days ago - 1 day' +%Y-%m-%d) end_date=$(date -d 'today' +%Y-%m-%d) -printf '%s commits between %s and %s\n' "${start_date}" "${end_date}" +printf '%s commits between %s and %s\n' "${last_month_commits}" "${start_date}" "${end_date}" # Retrieve merged PRs from the last month, paginated prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "closed:>$start_date closed:<$end_date" --json number,labels,title --limit "$((last_month_commits * 2))") From 8bb1097a5020cd8c1db981535e63fd6a76da6228 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 12:40:56 +0200 Subject: [PATCH 032/191] commits in range --- scripts/find_labels.sh | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 9177c0dab46df3..0e9f8f7cdc3ebc 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -15,16 +15,16 @@ one_month_ago=$(date -d '15 days ago' +%Y-%m-%d) git switch master -# find how many commits to master there have been in the last month -last_month_commits="$(git log --since="$one_month_ago" --pretty=oneline | wc -l)" - start_date=$(date -d '15 days ago - 1 day' +%Y-%m-%d) end_date=$(date -d 'today' +%Y-%m-%d) -printf '%s commits between %s and %s\n' "${last_month_commits}" "${start_date}" "${end_date}" +# find how many commits to master there have been in the last month +commits_in_range="$(git log --since="${start_date}" --until="${end_date}" --pretty=oneline | wc -l)" + +printf '%s commits between %s and %s\n' "${commits_in_range}" "${start_date}" "${end_date}" # Retrieve merged PRs from the last month, paginated -prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "closed:>$start_date closed:<$end_date" --json number,labels,title --limit "$((last_month_commits * 2))") +prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "closed:>$start_date closed:<$end_date" --json number,labels,title --limit "$((commits_in_range * 2))") # Check if any PRs are found if [ -z "$prs" ] || [ "$prs" = "[]" ]; then From 5c6aee83f4997f00ec1d6be8a4706c8437c3c4c0 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 12:45:51 +0200 Subject: [PATCH 033/191] prune --- scripts/find_labels.sh | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 0e9f8f7cdc3ebc..bcb172b160ba08 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -9,12 +9,9 @@ fi repo_owner=$1 repo_name=$2 -# Get the date for one month ago -one_month_ago=$(date -d '1 month ago' +%Y-%m-%d) -one_month_ago=$(date -d '15 days ago' +%Y-%m-%d) - git switch master +# Get the start and end dates start_date=$(date -d '15 days ago - 1 day' +%Y-%m-%d) end_date=$(date -d 'today' +%Y-%m-%d) @@ -26,10 +23,5 @@ printf '%s commits between %s and %s\n' "${commits_in_range}" "${start_date}" "$ # Retrieve merged PRs from the last month, paginated prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "closed:>$start_date closed:<$end_date" --json number,labels,title --limit "$((commits_in_range * 2))") -# Check if any PRs are found -if [ -z "$prs" ] || [ "$prs" = "[]" ]; then - break -fi - # Print PR numbers and their labels echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Title: \(.title)"' From 3cc12d2ec9bea00d34b360190289f64921c602c2 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 12:46:32 +0200 Subject: [PATCH 034/191] print closed --- scripts/find_labels.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index bcb172b160ba08..96df5f0d7d6d68 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -21,7 +21,7 @@ commits_in_range="$(git log --since="${start_date}" --until="${end_date}" --pret printf '%s commits between %s and %s\n' "${commits_in_range}" "${start_date}" "${end_date}" # Retrieve merged PRs from the last month, paginated -prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "closed:>$start_date closed:<$end_date" --json number,labels,title --limit "$((commits_in_range * 2))") +prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "closed:>$start_date closed:<$end_date" --json number,labels,title,closed --limit "$((commits_in_range * 2))") # Print PR numbers and their labels -echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Title: \(.title)"' +echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Closed: \(.closed) - Title: \(.title)"' From da61d9e30f9e48b18e5e73d4aa7196b7cc2e74f9 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 12:48:45 +0200 Subject: [PATCH 035/191] closedAt --- scripts/find_labels.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 96df5f0d7d6d68..2f19ff16ee6ef3 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -21,7 +21,7 @@ commits_in_range="$(git log --since="${start_date}" --until="${end_date}" --pret printf '%s commits between %s and %s\n' "${commits_in_range}" "${start_date}" "${end_date}" # Retrieve merged PRs from the last month, paginated -prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "closed:>$start_date closed:<$end_date" --json number,labels,title,closed --limit "$((commits_in_range * 2))") +prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "closedAt:>$start_date closedAt:<$end_date" --json number,labels,title,closedAt --limit "$((commits_in_range * 2))") # Print PR numbers and their labels -echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Closed: \(.closed) - Title: \(.title)"' +echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - ClosedAt: \(.closedAt) - Title: \(.title)"' From 3dc7d934830eec4d90c0b4e1b8c15b6cb3d9aada Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 12:50:55 +0200 Subject: [PATCH 036/191] restore closed --- scripts/find_labels.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 2f19ff16ee6ef3..96df5f0d7d6d68 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -21,7 +21,7 @@ commits_in_range="$(git log --since="${start_date}" --until="${end_date}" --pret printf '%s commits between %s and %s\n' "${commits_in_range}" "${start_date}" "${end_date}" # Retrieve merged PRs from the last month, paginated -prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "closedAt:>$start_date closedAt:<$end_date" --json number,labels,title,closedAt --limit "$((commits_in_range * 2))") +prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "closed:>$start_date closed:<$end_date" --json number,labels,title,closed --limit "$((commits_in_range * 2))") # Print PR numbers and their labels -echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - ClosedAt: \(.closedAt) - Title: \(.title)"' +echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Closed: \(.closed) - Title: \(.title)"' From 3a5dc18cc4be3ba9c75688cc96ebc4d4a26f39b7 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 12:55:44 +0200 Subject: [PATCH 037/191] range dates --- scripts/find_labels.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 96df5f0d7d6d68..d8bd902ecbfe81 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -21,7 +21,7 @@ commits_in_range="$(git log --since="${start_date}" --until="${end_date}" --pret printf '%s commits between %s and %s\n' "${commits_in_range}" "${start_date}" "${end_date}" # Retrieve merged PRs from the last month, paginated -prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "closed:>$start_date closed:<$end_date" --json number,labels,title,closed --limit "$((commits_in_range * 2))") +prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --closed "${start_date}T00:00:00..${end_date}T23:59:59" --json number,labels,title,closed --limit "$((commits_in_range * 2))") # Print PR numbers and their labels echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Closed: \(.closed) - Title: \(.title)"' From f33dcdde2e4ec3c2d3a546e4f0ae3c4f406e4d98 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 12:58:38 +0200 Subject: [PATCH 038/191] closedAt --- scripts/find_labels.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index d8bd902ecbfe81..146ab279417e57 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -21,7 +21,7 @@ commits_in_range="$(git log --since="${start_date}" --until="${end_date}" --pret printf '%s commits between %s and %s\n' "${commits_in_range}" "${start_date}" "${end_date}" # Retrieve merged PRs from the last month, paginated -prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --closed "${start_date}T00:00:00..${end_date}T23:59:59" --json number,labels,title,closed --limit "$((commits_in_range * 2))") +prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --closedAt "${start_date}T00:00:00..${end_date}T23:59:59" --json number,labels,title,closed --limit "$((commits_in_range * 2))") # Print PR numbers and their labels echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Closed: \(.closed) - Title: \(.title)"' From 5dd222c08dd7eb187d436b0ba4d4d983322a86c3 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 13:01:07 +0200 Subject: [PATCH 039/191] use search --- scripts/find_labels.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 146ab279417e57..42fdccfed8c513 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -21,7 +21,7 @@ commits_in_range="$(git log --since="${start_date}" --until="${end_date}" --pret printf '%s commits between %s and %s\n' "${commits_in_range}" "${start_date}" "${end_date}" # Retrieve merged PRs from the last month, paginated -prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --closedAt "${start_date}T00:00:00..${end_date}T23:59:59" --json number,labels,title,closed --limit "$((commits_in_range * 2))") +prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "${start_date}T00:00:00..${end_date}T23:59:59" --json number,labels,title,closed --limit "$((commits_in_range * 2))") # Print PR numbers and their labels echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Closed: \(.closed) - Title: \(.title)"' From 09c64748e40e273342690799aa1ea2cc670da690 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 13:02:13 +0200 Subject: [PATCH 040/191] search closed --- scripts/find_labels.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 42fdccfed8c513..649bf1c4dcdce4 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -21,7 +21,7 @@ commits_in_range="$(git log --since="${start_date}" --until="${end_date}" --pret printf '%s commits between %s and %s\n' "${commits_in_range}" "${start_date}" "${end_date}" # Retrieve merged PRs from the last month, paginated -prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "${start_date}T00:00:00..${end_date}T23:59:59" --json number,labels,title,closed --limit "$((commits_in_range * 2))") +prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "closed:${start_date}T00:00:00..${end_date}T23:59:59" --json number,labels,title,closed --limit "$((commits_in_range * 2))") # Print PR numbers and their labels echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Closed: \(.closed) - Title: \(.title)"' From d7abc43d3b26d53f112be3de7d7ce8d4b9963709 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 13:05:20 +0200 Subject: [PATCH 041/191] embed time in date --- scripts/find_labels.sh | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 649bf1c4dcdce4..cff53936b7d685 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -12,8 +12,8 @@ repo_name=$2 git switch master # Get the start and end dates -start_date=$(date -d '15 days ago - 1 day' +%Y-%m-%d) -end_date=$(date -d 'today' +%Y-%m-%d) +start_date="$(date -d '15 days ago - 1 day' +%Y-%m-%d)T00:00:00" +end_date="$(date -d 'today' +%Y-%m-%d)T23:59:59" # find how many commits to master there have been in the last month commits_in_range="$(git log --since="${start_date}" --until="${end_date}" --pretty=oneline | wc -l)" @@ -21,7 +21,7 @@ commits_in_range="$(git log --since="${start_date}" --until="${end_date}" --pret printf '%s commits between %s and %s\n' "${commits_in_range}" "${start_date}" "${end_date}" # Retrieve merged PRs from the last month, paginated -prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "closed:${start_date}T00:00:00..${end_date}T23:59:59" --json number,labels,title,closed --limit "$((commits_in_range * 2))") +prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "closed:${start_date}..${end_date}" --json number,labels,title,closed --limit "$((commits_in_range * 2))") # Print PR numbers and their labels echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Closed: \(.closed) - Title: \(.title)"' From d3eb548300c5d02894b9f1e4fda44d506cb5ff63 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 13:07:51 +0200 Subject: [PATCH 042/191] remove printing of closed --- scripts/find_labels.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index cff53936b7d685..3d5d1fb41bc814 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -21,7 +21,7 @@ commits_in_range="$(git log --since="${start_date}" --until="${end_date}" --pret printf '%s commits between %s and %s\n' "${commits_in_range}" "${start_date}" "${end_date}" # Retrieve merged PRs from the last month, paginated -prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "closed:${start_date}..${end_date}" --json number,labels,title,closed --limit "$((commits_in_range * 2))") +prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "closed:${start_date}..${end_date}" --json number,labels,title --limit "$((commits_in_range * 2))") # Print PR numbers and their labels -echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Closed: \(.closed) - Title: \(.title)"' +echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Title: \(.title)"' From bd13254a46bd603e49df24517e00419f7c5d4cce Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 13:17:35 +0200 Subject: [PATCH 043/191] print repository name --- .github/workflows/lint_and_suggest_pr.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/lint_and_suggest_pr.yml b/.github/workflows/lint_and_suggest_pr.yml index 1e2f0d6fc8812a..fc92fdaf960ac1 100644 --- a/.github/workflows/lint_and_suggest_pr.yml +++ b/.github/workflows/lint_and_suggest_pr.yml @@ -38,6 +38,7 @@ jobs: - name: blog report continue-on-error: true run: | + echo "repository: ${{ github.repository }}" ./scripts/find_labels.sh leanprover-community mathlib4 - name: lint From 1c6f6d479199ce1132f2ed6c02a5e125e45df7b8 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 13:22:17 +0200 Subject: [PATCH 044/191] use github API name for repo --- .github/workflows/lint_and_suggest_pr.yml | 2 +- scripts/find_labels.sh | 9 ++++----- 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/.github/workflows/lint_and_suggest_pr.yml b/.github/workflows/lint_and_suggest_pr.yml index fc92fdaf960ac1..f3a1c40e45e80b 100644 --- a/.github/workflows/lint_and_suggest_pr.yml +++ b/.github/workflows/lint_and_suggest_pr.yml @@ -39,7 +39,7 @@ jobs: continue-on-error: true run: | echo "repository: ${{ github.repository }}" - ./scripts/find_labels.sh leanprover-community mathlib4 + ./scripts/find_labels.sh "${{ github.repository }}" - name: lint continue-on-error: true # allows the following `reviewdog` step to add GitHub suggestions diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 3d5d1fb41bc814..416f27c4e05e39 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -1,13 +1,12 @@ #!/bin/bash # Check if required arguments are provided -if [ "$#" -ne 2 ]; then - echo "Usage: $0 " +if [ "$#" -ne 1 ]; then + printf $'Usage: %s \n\nFor instance `%s leanprover-community/mathlib4`\n\n' "${0}" "${0}" exit 1 fi -repo_owner=$1 -repo_name=$2 +repository=$1 git switch master @@ -21,7 +20,7 @@ commits_in_range="$(git log --since="${start_date}" --until="${end_date}" --pret printf '%s commits between %s and %s\n' "${commits_in_range}" "${start_date}" "${end_date}" # Retrieve merged PRs from the last month, paginated -prs=$(gh pr list --repo "$repo_owner/$repo_name" --state closed --search "closed:${start_date}..${end_date}" --json number,labels,title --limit "$((commits_in_range * 2))") +prs=$(gh pr list --repo "$repository" --state closed --search "closed:${start_date}..${end_date}" --json number,labels,title --limit "$((commits_in_range * 2))") # Print PR numbers and their labels echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Title: \(.title)"' From 88882aee255f6dc18c41a4fbf262c35ceb66e01e Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 13:24:42 +0200 Subject: [PATCH 045/191] Capitalize Repository --- .github/workflows/lint_and_suggest_pr.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/lint_and_suggest_pr.yml b/.github/workflows/lint_and_suggest_pr.yml index f3a1c40e45e80b..a31f262b305c67 100644 --- a/.github/workflows/lint_and_suggest_pr.yml +++ b/.github/workflows/lint_and_suggest_pr.yml @@ -38,7 +38,7 @@ jobs: - name: blog report continue-on-error: true run: | - echo "repository: ${{ github.repository }}" + echo "Repository: ${{ github.repository }}" ./scripts/find_labels.sh "${{ github.repository }}" - name: lint From 0bbb60be44d1acbc44bbe4153075aa97ae771266 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 13:41:17 +0200 Subject: [PATCH 046/191] base on master --- scripts/find_labels.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 416f27c4e05e39..d7e5d2de19138d 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -20,7 +20,7 @@ commits_in_range="$(git log --since="${start_date}" --until="${end_date}" --pret printf '%s commits between %s and %s\n' "${commits_in_range}" "${start_date}" "${end_date}" # Retrieve merged PRs from the last month, paginated -prs=$(gh pr list --repo "$repository" --state closed --search "closed:${start_date}..${end_date}" --json number,labels,title --limit "$((commits_in_range * 2))") +prs=$(gh pr list --repo "$repository" --state closed --base master --search "closed:${start_date}..${end_date}" --json number,labels,title --limit "$((commits_in_range * 2))") # Print PR numbers and their labels echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Title: \(.title)"' From f010c98a82a4b384fab75e11f090c27b2b1768ec Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 13:53:33 +0200 Subject: [PATCH 047/191] report missed PRs --- scripts/find_labels.sh | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index d7e5d2de19138d..7d75275d0d7459 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -23,4 +23,13 @@ printf '%s commits between %s and %s\n' "${commits_in_range}" "${start_date}" "$ prs=$(gh pr list --repo "$repository" --state closed --base master --search "closed:${start_date}..${end_date}" --json number,labels,title --limit "$((commits_in_range * 2))") # Print PR numbers and their labels -echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Title: \(.title)"' +prs_to_print="$(echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Title: \(.title)"')" + +echo "${prs_to_print}" + +echo "PRs not corresponding to a commit:" +comm -23 <(echo "${prs_to_print}" | awk '{print $2}' mwe_outputs/prBlog.txt | sort) <(git log --pretty=oneline --since="$(date -d '15 days ago - 1 day' +%Y-%m-%d)T00:00:00" --until="$(date -d 'today' +%Y-%m-%d)T23:59:59" | sed -n 's=.*(\(#[0-9]*\))$=\1=p' | sort) + +echo 'PRs not found by `gh`' +comm -23 <(echo "${prs_to_print}" | awk '{print $2}' mwe_outputs/prBlog.txt | sort) <(git log --pretty=oneline --since="$(date -d '15 days ago - 1 day' +%Y-%m-%d)T00:00:00" --until="$(date -d 'today' +%Y-%m-%d)T23:59:59" | sed -n 's=.*(\(#[0-9]*\))$=\1=p' | sort) +printf $'\n---\n' From 5b022b31494e323d0bc538efd7fcbae16a66a2ae Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 13:55:53 +0200 Subject: [PATCH 048/191] fix --- scripts/find_labels.sh | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 7d75275d0d7459..b57c034e437e0f 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -27,9 +27,11 @@ prs_to_print="$(echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged b echo "${prs_to_print}" -echo "PRs not corresponding to a commit:" -comm -23 <(echo "${prs_to_print}" | awk '{print $2}' mwe_outputs/prBlog.txt | sort) <(git log --pretty=oneline --since="$(date -d '15 days ago - 1 day' +%Y-%m-%d)T00:00:00" --until="$(date -d 'today' +%Y-%m-%d)T23:59:59" | sed -n 's=.*(\(#[0-9]*\))$=\1=p' | sort) +printf $'\nPRs not corresponding to a commit\n\n' -echo 'PRs not found by `gh`' -comm -23 <(echo "${prs_to_print}" | awk '{print $2}' mwe_outputs/prBlog.txt | sort) <(git log --pretty=oneline --since="$(date -d '15 days ago - 1 day' +%Y-%m-%d)T00:00:00" --until="$(date -d 'today' +%Y-%m-%d)T23:59:59" | sed -n 's=.*(\(#[0-9]*\))$=\1=p' | sort) +comm -23 <(echo "${prs_to_print}" | awk '{print $2}' | sort) <(git log --pretty=oneline --since="$(date -d '15 days ago - 1 day' +%Y-%m-%d)T00:00:00" --until="$(date -d 'today' +%Y-%m-%d)T23:59:59" | sed -n 's=.*(\(#[0-9]*\))$=\1=p' | sort) + +printf $'PRs not found by `gh`\n\n' + +comm -23 <(echo "${prs_to_print}" | awk '{print $2}' | sort) <(git log --pretty=oneline --since="$(date -d '15 days ago - 1 day' +%Y-%m-%d)T00:00:00" --until="$(date -d 'today' +%Y-%m-%d)T23:59:59" | sed -n 's=.*(\(#[0-9]*\))$=\1=p' | sort) printf $'\n---\n' From 941964b62aa1b68083fbf736e4488077214f72d9 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 13:57:19 +0200 Subject: [PATCH 049/191] dates in git --- scripts/find_labels.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index b57c034e437e0f..fd588e978bc866 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -29,9 +29,9 @@ echo "${prs_to_print}" printf $'\nPRs not corresponding to a commit\n\n' -comm -23 <(echo "${prs_to_print}" | awk '{print $2}' | sort) <(git log --pretty=oneline --since="$(date -d '15 days ago - 1 day' +%Y-%m-%d)T00:00:00" --until="$(date -d 'today' +%Y-%m-%d)T23:59:59" | sed -n 's=.*(\(#[0-9]*\))$=\1=p' | sort) +comm -23 <(echo "${prs_to_print}" | awk '{print $2}' | sort) <(git log --pretty=oneline --since="${start_date}" --until="${end_date}" | sed -n 's=.*(\(#[0-9]*\))$=\1=p' | sort) printf $'PRs not found by `gh`\n\n' -comm -23 <(echo "${prs_to_print}" | awk '{print $2}' | sort) <(git log --pretty=oneline --since="$(date -d '15 days ago - 1 day' +%Y-%m-%d)T00:00:00" --until="$(date -d 'today' +%Y-%m-%d)T23:59:59" | sed -n 's=.*(\(#[0-9]*\))$=\1=p' | sort) +comm -23 <(echo "${prs_to_print}" | awk '{print $2}' | sort) <(git log --pretty=oneline --since="${start_date}" --until="${end_date}" | sed -n 's=.*(\(#[0-9]*\))$=\1=p' | sort) printf $'\n---\n' From 2d09ba438e1d563e4507b6ca34bf7cb9cb8b02ff Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 14:00:22 +0200 Subject: [PATCH 050/191] engulph --- scripts/find_labels.sh | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index fd588e978bc866..5a729a6bc97708 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -27,9 +27,7 @@ prs_to_print="$(echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged b echo "${prs_to_print}" -printf $'\nPRs not corresponding to a commit\n\n' - -comm -23 <(echo "${prs_to_print}" | awk '{print $2}' | sort) <(git log --pretty=oneline --since="${start_date}" --until="${end_date}" | sed -n 's=.*(\(#[0-9]*\))$=\1=p' | sort) +printf $'\nPRs not corresponding to a commit\n\n\'%s\'\n' "$(comm -23 <(echo "${prs_to_print}" | awk '{print $2}' | sort) <(git log --pretty=oneline --since="${start_date}" --until="${end_date}" | sed -n 's=.*(\(#[0-9]*\))$=\1=p' | sort))" printf $'PRs not found by `gh`\n\n' From eaa539826f81dab2c0ac8beaf2bdf66d96d78b67 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 14:03:33 +0200 Subject: [PATCH 051/191] both --- scripts/find_labels.sh | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 5a729a6bc97708..13921b4c77e637 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -27,9 +27,12 @@ prs_to_print="$(echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged b echo "${prs_to_print}" -printf $'\nPRs not corresponding to a commit\n\n\'%s\'\n' "$(comm -23 <(echo "${prs_to_print}" | awk '{print $2}' | sort) <(git log --pretty=oneline --since="${start_date}" --until="${end_date}" | sed -n 's=.*(\(#[0-9]*\))$=\1=p' | sort))" +only_gh="$(comm -23 <(echo "${prs_to_print}" | awk '{print $2}' | sort) <(git log --pretty=oneline --since="${start_date}" --until="${end_date}" | sed -n 's=.*(\(#[0-9]*\))$=\1=p' | sort))" -printf $'PRs not found by `gh`\n\n' +only_git="$(comm -13 <(echo "${prs_to_print}" | awk '{print $2}' | sort) <(git log --pretty=oneline --since="${start_date}" --until="${end_date}" | sed -n 's=.*(\(#[0-9]*\))$=\1=p' | sort))" + +printf $'\nPRs not corresponding to a commit\n\n\'%s\'\n' "${only_gh}" + +printf $'PRs not found by `gh`\n\n\'%s\'\n' "${only_git}" -comm -23 <(echo "${prs_to_print}" | awk '{print $2}' | sort) <(git log --pretty=oneline --since="${start_date}" --until="${end_date}" | sed -n 's=.*(\(#[0-9]*\))$=\1=p' | sort) printf $'\n---\n' From b3358bc43ff13cf79bb6a9b16db0e3b63289582a Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 14:10:14 +0200 Subject: [PATCH 052/191] better reporting --- scripts/find_labels.sh | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 13921b4c77e637..7962a22d69fdac 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -31,8 +31,20 @@ only_gh="$(comm -23 <(echo "${prs_to_print}" | awk '{print $2}' | sort) <(git lo only_git="$(comm -13 <(echo "${prs_to_print}" | awk '{print $2}' | sort) <(git log --pretty=oneline --since="${start_date}" --until="${end_date}" | sed -n 's=.*(\(#[0-9]*\))$=\1=p' | sort))" -printf $'\nPRs not corresponding to a commit\n\n\'%s\'\n' "${only_gh}" +printf $'\n\nReports\n\n---\n' -printf $'PRs not found by `gh`\n\n\'%s\'\n' "${only_git}" +if [ -z "${only_gh}" ] +then + printf $'\nAll PRs are accounted for!\n' +else + printf $'\nPRs not corresponding to a commit\n\n\'%s\'\n' "${only_gh}" +fi + +if [ -z "${only_git}" ] +then + printf $'\nAll commits are accounted for!\n' +else + printf $'PRs not found by `gh`\n\n\'%s\'\n' "${only_git}" +fi printf $'\n---\n' From 53da2c4493c3b91be78b0a8a16e64a72efbac5b7 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 14:13:43 +0200 Subject: [PATCH 053/191] formatting --- scripts/find_labels.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 7962a22d69fdac..3cae33475069e1 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -17,7 +17,7 @@ end_date="$(date -d 'today' +%Y-%m-%d)T23:59:59" # find how many commits to master there have been in the last month commits_in_range="$(git log --since="${start_date}" --until="${end_date}" --pretty=oneline | wc -l)" -printf '%s commits between %s and %s\n' "${commits_in_range}" "${start_date}" "${end_date}" +printf $'\n%s commits between %s and %s\n' "${commits_in_range}" "${start_date}" "${end_date}" # Retrieve merged PRs from the last month, paginated prs=$(gh pr list --repo "$repository" --state closed --base master --search "closed:${start_date}..${end_date}" --json number,labels,title --limit "$((commits_in_range * 2))") @@ -31,7 +31,7 @@ only_gh="$(comm -23 <(echo "${prs_to_print}" | awk '{print $2}' | sort) <(git lo only_git="$(comm -13 <(echo "${prs_to_print}" | awk '{print $2}' | sort) <(git log --pretty=oneline --since="${start_date}" --until="${end_date}" | sed -n 's=.*(\(#[0-9]*\))$=\1=p' | sort))" -printf $'\n\nReports\n\n---\n' +printf $'\nReports\n\n---\n' if [ -z "${only_gh}" ] then From f6fca31633464accd47f77f653ea46c8202c262a Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 14:15:52 +0200 Subject: [PATCH 054/191] separation --- scripts/find_labels.sh | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 3cae33475069e1..1ffe74a59beec3 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -31,20 +31,20 @@ only_gh="$(comm -23 <(echo "${prs_to_print}" | awk '{print $2}' | sort) <(git lo only_git="$(comm -13 <(echo "${prs_to_print}" | awk '{print $2}' | sort) <(git log --pretty=oneline --since="${start_date}" --until="${end_date}" | sed -n 's=.*(\(#[0-9]*\))$=\1=p' | sort))" -printf $'\nReports\n\n---\n' +printf $'\n---\nReports\n\n' if [ -z "${only_gh}" ] then - printf $'\nAll PRs are accounted for!\n' + printf $'\n* All PRs are accounted for!\n' else - printf $'\nPRs not corresponding to a commit\n\n\'%s\'\n' "${only_gh}" + printf $'\n* PRs not corresponding to a commit\n\n\'%s\'\n' "${only_gh}" fi if [ -z "${only_git}" ] then - printf $'\nAll commits are accounted for!\n' + printf $'\n* All commits are accounted for!\n' else - printf $'PRs not found by `gh`\n\n\'%s\'\n' "${only_git}" + printf $'* PRs not found by `gh`\n\n\'%s\'\n' "${only_git}" fi printf $'\n---\n' From bf8180e6a84ec2299b4d8e2ebd2d0ce2fc4023d2 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 14:23:59 +0200 Subject: [PATCH 055/191] switch back to original branch --- scripts/find_labels.sh | 2 ++ 1 file changed, 2 insertions(+) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 1ffe74a59beec3..0942b97754f890 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -48,3 +48,5 @@ else fi printf $'\n---\n' + +git switch - From e9e4bf5d82311f3cb256ba5e8bc8449b50bae21d Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 14:26:53 +0200 Subject: [PATCH 056/191] switch back to original branch --- scripts/find_labels.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 0942b97754f890..0fac8990ad1954 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -47,6 +47,6 @@ else printf $'* PRs not found by `gh`\n\n\'%s\'\n' "${only_git}" fi -printf $'\n---\n' +printf $'\n---\n%s\n' "${{ github.head_ref }}" -git switch - +git switch - || git switch "${{ github.head_ref }}" From 8bd675ae52247baf1e99b8f2a216b75b1c049dc8 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 14:28:32 +0200 Subject: [PATCH 057/191] checkout --- scripts/find_labels.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 0fac8990ad1954..e442e6758bc34d 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -49,4 +49,4 @@ fi printf $'\n---\n%s\n' "${{ github.head_ref }}" -git switch - || git switch "${{ github.head_ref }}" +git checkout - || git switch "${{ github.head_ref }}" From 5424675f0024a98d830c2535de473e0560a3655b Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 14:31:41 +0200 Subject: [PATCH 058/191] print branch name --- .github/workflows/lint_and_suggest_pr.yml | 2 +- scripts/find_labels.sh | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/lint_and_suggest_pr.yml b/.github/workflows/lint_and_suggest_pr.yml index a31f262b305c67..76474e1c431f79 100644 --- a/.github/workflows/lint_and_suggest_pr.yml +++ b/.github/workflows/lint_and_suggest_pr.yml @@ -38,7 +38,7 @@ jobs: - name: blog report continue-on-error: true run: | - echo "Repository: ${{ github.repository }}" + printf $'Repository: %s\nBranch: %s\n' "${{ github.repository }}" "${{ github.head_ref }}" ./scripts/find_labels.sh "${{ github.repository }}" - name: lint diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index e442e6758bc34d..5ed335f3e8cd27 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -47,6 +47,6 @@ else printf $'* PRs not found by `gh`\n\n\'%s\'\n' "${only_git}" fi -printf $'\n---\n%s\n' "${{ github.head_ref }}" +printf $'\n---\n' -git checkout - || git switch "${{ github.head_ref }}" +git checkout - From bee9d5527cba549dc0c6de849fd68b6ca8c61c7b Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 14:37:26 +0200 Subject: [PATCH 059/191] use BRANCH_NAME as env variable --- .github/workflows/lint_and_suggest_pr.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/lint_and_suggest_pr.yml b/.github/workflows/lint_and_suggest_pr.yml index 76474e1c431f79..e46186292a645c 100644 --- a/.github/workflows/lint_and_suggest_pr.yml +++ b/.github/workflows/lint_and_suggest_pr.yml @@ -13,6 +13,7 @@ jobs: env: GH_TOKEN: ${{ github.token }} + BRANCH_NAME: ${{ github.head_ref }} steps: - name: cleanup @@ -38,7 +39,7 @@ jobs: - name: blog report continue-on-error: true run: | - printf $'Repository: %s\nBranch: %s\n' "${{ github.repository }}" "${{ github.head_ref }}" + printf $'Repository: %s\nBranch: %s\n' "${{ github.repository }}" "${BRANCH_NAME}" ./scripts/find_labels.sh "${{ github.repository }}" - name: lint From 9cfdaf1b15d3e8b1f83dcb5269ea66408a94d40a Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 14:45:40 +0200 Subject: [PATCH 060/191] create and remove temp files --- scripts/find_labels.sh | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 5ed335f3e8cd27..61c084b08716a1 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -27,9 +27,14 @@ prs_to_print="$(echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged b echo "${prs_to_print}" -only_gh="$(comm -23 <(echo "${prs_to_print}" | awk '{print $2}' | sort) <(git log --pretty=oneline --since="${start_date}" --until="${end_date}" | sed -n 's=.*(\(#[0-9]*\))$=\1=p' | sort))" +echo "${prs_to_print}" | awk '{print $2}' | sort > found_by_gh.txt +git log --pretty=oneline --since="${start_date}" --until="${end_date}" | + sed -n 's=.*(\(#[0-9]*\))$=\1=p' | sort > found_by_git.txt -only_git="$(comm -13 <(echo "${prs_to_print}" | awk '{print $2}' | sort) <(git log --pretty=oneline --since="${start_date}" --until="${end_date}" | sed -n 's=.*(\(#[0-9]*\))$=\1=p' | sort))" +only_gh="$( comm -23 found_by_gh.txt found_by_git.txt)" +only_git="$(comm -13 found_by_gh.txt found_by_git.txt)" + +rm -rf found_by_gh.txt found_by_git.txt printf $'\n---\nReports\n\n' From d4c6b83842d42ba38d968d61a8470ab73e86ab69 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 14:48:55 +0200 Subject: [PATCH 061/191] print PRs --- scripts/find_labels.sh | 2 ++ 1 file changed, 2 insertions(+) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 61c084b08716a1..2adad22c65c8a1 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -27,6 +27,8 @@ prs_to_print="$(echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged b echo "${prs_to_print}" +echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "(#\(.number))"' + echo "${prs_to_print}" | awk '{print $2}' | sort > found_by_gh.txt git log --pretty=oneline --since="${start_date}" --until="${end_date}" | sed -n 's=.*(\(#[0-9]*\))$=\1=p' | sort > found_by_git.txt From 2cb4eda3b214d7f7b0b2015ebdc301c668954481 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 14:55:00 +0200 Subject: [PATCH 062/191] refactor --- scripts/find_labels.sh | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 2adad22c65c8a1..bc7bddce01dfb5 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -23,15 +23,11 @@ printf $'\n%s commits between %s and %s\n' "${commits_in_range}" "${start_date}" prs=$(gh pr list --repo "$repository" --state closed --base master --search "closed:${start_date}..${end_date}" --json number,labels,title --limit "$((commits_in_range * 2))") # Print PR numbers and their labels -prs_to_print="$(echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Title: \(.title)"')" +echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Title: \(.title)"' -echo "${prs_to_print}" - -echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "(#\(.number))"' - -echo "${prs_to_print}" | awk '{print $2}' | sort > found_by_gh.txt +echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "(#\(.number))"' | sort > found_by_gh.txt git log --pretty=oneline --since="${start_date}" --until="${end_date}" | - sed -n 's=.*(\(#[0-9]*\))$=\1=p' | sort > found_by_git.txt + sed -n 's=.*\((#[0-9]*)\)$=\1=p' | sort > found_by_git.txt only_gh="$( comm -23 found_by_gh.txt found_by_git.txt)" only_git="$(comm -13 found_by_gh.txt found_by_git.txt)" From 53557eab90dd6689051b6b4b162c92bbc42d515a Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 15:21:56 +0200 Subject: [PATCH 063/191] start extracting dates and docs --- scripts/find_labels.sh | 20 ++++++++++++++------ 1 file changed, 14 insertions(+), 6 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index bc7bddce01dfb5..abc4c9af405a83 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -6,26 +6,31 @@ if [ "$#" -ne 1 ]; then exit 1 fi -repository=$1 +findInRange () { -git switch master +repository="${1}" # Get the start and end dates -start_date="$(date -d '15 days ago - 1 day' +%Y-%m-%d)T00:00:00" -end_date="$(date -d 'today' +%Y-%m-%d)T23:59:59" +start_date="${2}" +end_date="${3}" + +git switch master # find how many commits to master there have been in the last month commits_in_range="$(git log --since="${start_date}" --until="${end_date}" --pretty=oneline | wc -l)" printf $'\n%s commits between %s and %s\n' "${commits_in_range}" "${start_date}" "${end_date}" -# Retrieve merged PRs from the last month, paginated +# Retrieve merged PRs from the given range prs=$(gh pr list --repo "$repository" --state closed --base master --search "closed:${start_date}..${end_date}" --json number,labels,title --limit "$((commits_in_range * 2))") -# Print PR numbers and their labels +# Print PR numbers, their labels and their title echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Title: \(.title)"' +# Store the PR numbers, as found by `gh` echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "(#\(.number))"' | sort > found_by_gh.txt + +# Store the PR numbers, as found by looking at the commits to `master` git log --pretty=oneline --since="${start_date}" --until="${end_date}" | sed -n 's=.*\((#[0-9]*)\)$=\1=p' | sort > found_by_git.txt @@ -53,3 +58,6 @@ fi printf $'\n---\n' git checkout - +} + +findInRange "${1}" "$(date -d '15 days ago - 1 day' +%Y-%m-%d)T00:00:00" "$(date -d 'today' +%Y-%m-%d)T23:59:59" From 60d2eaba30b4ac4000e039cf69ee34dc6f81b9ff Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 15:24:57 +0200 Subject: [PATCH 064/191] extract reports --- scripts/find_labels.sh | 22 ++++++++++++---------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index abc4c9af405a83..9c97635d88fa91 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -6,6 +6,8 @@ if [ "$#" -ne 1 ]; then exit 1 fi +rm -rf found_by_gh.txt found_by_git.txt + findInRange () { repository="${1}" @@ -27,18 +29,21 @@ prs=$(gh pr list --repo "$repository" --state closed --base master --search "clo # Print PR numbers, their labels and their title echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Title: \(.title)"' -# Store the PR numbers, as found by `gh` -echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "(#\(.number))"' | sort > found_by_gh.txt +# Store to file `found_by_gh.txt` the PR numbers, as found by `gh` +echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "(#\(.number))"' | sort >> found_by_gh.txt -# Store the PR numbers, as found by looking at the commits to `master` +# Store to file `found_by_git.txt` the PR numbers, as found by looking at the commits to `master` git log --pretty=oneline --since="${start_date}" --until="${end_date}" | - sed -n 's=.*\((#[0-9]*)\)$=\1=p' | sort > found_by_git.txt + sed -n 's=.*\((#[0-9]*)\)$=\1=p' | sort >> found_by_git.txt + +git checkout - +} + +findInRange "${1}" "$(date -d '15 days ago - 1 day' +%Y-%m-%d)T00:00:00" "$(date -d 'today' +%Y-%m-%d)T23:59:59" only_gh="$( comm -23 found_by_gh.txt found_by_git.txt)" only_git="$(comm -13 found_by_gh.txt found_by_git.txt)" -rm -rf found_by_gh.txt found_by_git.txt - printf $'\n---\nReports\n\n' if [ -z "${only_gh}" ] @@ -57,7 +62,4 @@ fi printf $'\n---\n' -git checkout - -} - -findInRange "${1}" "$(date -d '15 days ago - 1 day' +%Y-%m-%d)T00:00:00" "$(date -d 'today' +%Y-%m-%d)T23:59:59" +rm -rf found_by_gh.txt found_by_git.txt From 1b5ccb947c92baa1c9231bb1277946a95357890a Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 15:26:25 +0200 Subject: [PATCH 065/191] checkout outside of the function --- scripts/find_labels.sh | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 9c97635d88fa91..c2877b9b5c6968 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -6,6 +6,8 @@ if [ "$#" -ne 1 ]; then exit 1 fi +git switch master + rm -rf found_by_gh.txt found_by_git.txt findInRange () { @@ -16,8 +18,6 @@ repository="${1}" start_date="${2}" end_date="${3}" -git switch master - # find how many commits to master there have been in the last month commits_in_range="$(git log --since="${start_date}" --until="${end_date}" --pretty=oneline | wc -l)" @@ -35,8 +35,6 @@ echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "(# # Store to file `found_by_git.txt` the PR numbers, as found by looking at the commits to `master` git log --pretty=oneline --since="${start_date}" --until="${end_date}" | sed -n 's=.*\((#[0-9]*)\)$=\1=p' | sort >> found_by_git.txt - -git checkout - } findInRange "${1}" "$(date -d '15 days ago - 1 day' +%Y-%m-%d)T00:00:00" "$(date -d 'today' +%Y-%m-%d)T23:59:59" @@ -63,3 +61,5 @@ fi printf $'\n---\n' rm -rf found_by_gh.txt found_by_git.txt + +git checkout - From 42cc216378b620049c3d329393f63a87c6d0b828 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 15:29:26 +0200 Subject: [PATCH 066/191] run twice to cover a whole month --- scripts/find_labels.sh | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index c2877b9b5c6968..33b3f50902ef56 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -37,7 +37,8 @@ git log --pretty=oneline --since="${start_date}" --until="${end_date}" | sed -n 's=.*\((#[0-9]*)\)$=\1=p' | sort >> found_by_git.txt } -findInRange "${1}" "$(date -d '15 days ago - 1 day' +%Y-%m-%d)T00:00:00" "$(date -d 'today' +%Y-%m-%d)T23:59:59" +findInRange "${1}" '2024-07-01T00:00:00' '2024-07-15T23:59:59' +findInRange "${1}" '2024-07-16T00:00:00' "$(date -d '2024-07-01 + 1 month - 1 day' +%Y-%m-%d)T23:59:59" only_gh="$( comm -23 found_by_gh.txt found_by_git.txt)" only_git="$(comm -13 found_by_gh.txt found_by_git.txt)" From 360d2f827e70b7adf0a3a123cf3f7c74f1512773 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 15:31:52 +0200 Subject: [PATCH 067/191] sort --- scripts/find_labels.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 33b3f50902ef56..1b174329b450a7 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -40,8 +40,8 @@ git log --pretty=oneline --since="${start_date}" --until="${end_date}" | findInRange "${1}" '2024-07-01T00:00:00' '2024-07-15T23:59:59' findInRange "${1}" '2024-07-16T00:00:00' "$(date -d '2024-07-01 + 1 month - 1 day' +%Y-%m-%d)T23:59:59" -only_gh="$( comm -23 found_by_gh.txt found_by_git.txt)" -only_git="$(comm -13 found_by_gh.txt found_by_git.txt)" +only_gh="$( comm -23 <(sort found_by_gh.txt) <(sort found_by_git.txt))" +only_git="$(comm -13 <(sort found_by_gh.txt) <(sort found_by_git.txt))" printf $'\n---\nReports\n\n' From 3c18faad6360800196227d1f4716e1ce53e3a168 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 15:36:02 +0200 Subject: [PATCH 068/191] commit in range once --- scripts/find_labels.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 1b174329b450a7..6cedc913a8af18 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -21,8 +21,6 @@ end_date="${3}" # find how many commits to master there have been in the last month commits_in_range="$(git log --since="${start_date}" --until="${end_date}" --pretty=oneline | wc -l)" -printf $'\n%s commits between %s and %s\n' "${commits_in_range}" "${start_date}" "${end_date}" - # Retrieve merged PRs from the given range prs=$(gh pr list --repo "$repository" --state closed --base master --search "closed:${start_date}..${end_date}" --json number,labels,title --limit "$((commits_in_range * 2))") @@ -37,6 +35,8 @@ git log --pretty=oneline --since="${start_date}" --until="${end_date}" | sed -n 's=.*\((#[0-9]*)\)$=\1=p' | sort >> found_by_git.txt } +commits_in_range="$(git log --since=2024-07-01T00:00:00 --until="$(date -d '2024-07-01 + 1 month - 1 day' +%Y-%m-%d)T23:59:59" --pretty=oneline | wc -l)" + findInRange "${1}" '2024-07-01T00:00:00' '2024-07-15T23:59:59' findInRange "${1}" '2024-07-16T00:00:00' "$(date -d '2024-07-01 + 1 month - 1 day' +%Y-%m-%d)T23:59:59" From 93f0a06d7382cd2fa06547f0cd582302edc78ece Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 16:04:33 +0200 Subject: [PATCH 069/191] print commits in range --- scripts/find_labels.sh | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 6cedc913a8af18..9e834ec47d2164 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -35,7 +35,12 @@ git log --pretty=oneline --since="${start_date}" --until="${end_date}" | sed -n 's=.*\((#[0-9]*)\)$=\1=p' | sort >> found_by_git.txt } -commits_in_range="$(git log --since=2024-07-01T00:00:00 --until="$(date -d '2024-07-01 + 1 month - 1 day' +%Y-%m-%d)T23:59:59" --pretty=oneline | wc -l)" +start_date=2024-07-01T00:00:00 +end_date="$(date -d '2024-07-01 + 1 month - 1 day' +%Y-%m-%d)T23:59:59" + +commits_in_range="$(git log --since="${start_date}" --until="${end_date}" --pretty=oneline | wc -l)" + +printf $'\n%s commits between %s and %s\n' "${commits_in_range}" "${start_date}" "${end_date}" findInRange "${1}" '2024-07-01T00:00:00' '2024-07-15T23:59:59' findInRange "${1}" '2024-07-16T00:00:00' "$(date -d '2024-07-01 + 1 month - 1 day' +%Y-%m-%d)T23:59:59" From 923b3ec5a74404644faa8c59115ae66ed9267e36 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 16:41:15 +0200 Subject: [PATCH 070/191] remove ticks --- scripts/find_labels.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 9e834ec47d2164..a76f92014f6cdd 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -54,14 +54,14 @@ if [ -z "${only_gh}" ] then printf $'\n* All PRs are accounted for!\n' else - printf $'\n* PRs not corresponding to a commit\n\n\'%s\'\n' "${only_gh}" + printf $'\n* PRs not corresponding to a commit\n\n%s\n' "${only_gh}" fi if [ -z "${only_git}" ] then printf $'\n* All commits are accounted for!\n' else - printf $'* PRs not found by `gh`\n\n\'%s\'\n' "${only_git}" + printf $'* PRs not found by `gh`\n\n%s\n' "${only_git}" fi printf $'\n---\n' From 3a56678cdf19aafd16b14631646d53e89f2946d7 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 17:19:34 +0200 Subject: [PATCH 071/191] abstract year month --- scripts/find_labels.sh | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index a76f92014f6cdd..74b78f20aac63a 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -35,15 +35,17 @@ git log --pretty=oneline --since="${start_date}" --until="${end_date}" | sed -n 's=.*\((#[0-9]*)\)$=\1=p' | sort >> found_by_git.txt } -start_date=2024-07-01T00:00:00 -end_date="$(date -d '2024-07-01 + 1 month - 1 day' +%Y-%m-%d)T23:59:59" +yr_mth=2024-07 + +start_date="${yr_mth}-01T00:00:00" +end_date="$(date -d "${yr_mth}-01 + 1 month - 1 day" +%Y-%m-%d)T23:59:59" commits_in_range="$(git log --since="${start_date}" --until="${end_date}" --pretty=oneline | wc -l)" printf $'\n%s commits between %s and %s\n' "${commits_in_range}" "${start_date}" "${end_date}" -findInRange "${1}" '2024-07-01T00:00:00' '2024-07-15T23:59:59' -findInRange "${1}" '2024-07-16T00:00:00' "$(date -d '2024-07-01 + 1 month - 1 day' +%Y-%m-%d)T23:59:59" +findInRange "${1}" "${yr_mth}-01T00:00:00" "${yr_mth}-15T23:59:59" +findInRange "${1}" "${yr_mth}-16T00:00:00" "$(date -d "${yr_mth}-01 + 1 month - 1 day" +%Y-%m-%d)T23:59:59" only_gh="$( comm -23 <(sort found_by_gh.txt) <(sort found_by_git.txt))" only_git="$(comm -13 <(sort found_by_gh.txt) <(sort found_by_git.txt))" From a2e68b4182b810d39576e6395a8db2958dfa7b90 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 17:33:32 +0200 Subject: [PATCH 072/191] recycle variable --- scripts/find_labels.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 74b78f20aac63a..49ad8eb7b3e78f 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -44,8 +44,8 @@ commits_in_range="$(git log --since="${start_date}" --until="${end_date}" --pret printf $'\n%s commits between %s and %s\n' "${commits_in_range}" "${start_date}" "${end_date}" -findInRange "${1}" "${yr_mth}-01T00:00:00" "${yr_mth}-15T23:59:59" -findInRange "${1}" "${yr_mth}-16T00:00:00" "$(date -d "${yr_mth}-01 + 1 month - 1 day" +%Y-%m-%d)T23:59:59" +findInRange "${1}" "${start_date}" "${yr_mth}-15T23:59:59" +findInRange "${1}" "${yr_mth}-16T00:00:00" "${end_date}" only_gh="$( comm -23 <(sort found_by_gh.txt) <(sort found_by_git.txt))" only_git="$(comm -13 <(sort found_by_gh.txt) <(sort found_by_git.txt))" From 503191150bec8c439edcbbdc7bef3ee4cf07fb41 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 17:37:27 +0200 Subject: [PATCH 073/191] local vars --- scripts/find_labels.sh | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 49ad8eb7b3e78f..85d67370e67c1d 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -15,14 +15,14 @@ findInRange () { repository="${1}" # Get the start and end dates -start_date="${2}" -end_date="${3}" +startDate="${2}" +endDate="${3}" # find how many commits to master there have been in the last month -commits_in_range="$(git log --since="${start_date}" --until="${end_date}" --pretty=oneline | wc -l)" +commits_in_range="$(git log --since="${startDate}" --until="${endDate}" --pretty=oneline | wc -l)" # Retrieve merged PRs from the given range -prs=$(gh pr list --repo "$repository" --state closed --base master --search "closed:${start_date}..${end_date}" --json number,labels,title --limit "$((commits_in_range * 2))") +prs=$(gh pr list --repo "$repository" --state closed --base master --search "closed:${startDate}..${endDate}" --json number,labels,title --limit "$((commits_in_range * 2))") # Print PR numbers, their labels and their title echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Title: \(.title)"' @@ -31,7 +31,7 @@ echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "(#\(.number))"' | sort >> found_by_gh.txt # Store to file `found_by_git.txt` the PR numbers, as found by looking at the commits to `master` -git log --pretty=oneline --since="${start_date}" --until="${end_date}" | +git log --pretty=oneline --since="${startDate}" --until="${endDate}" | sed -n 's=.*\((#[0-9]*)\)$=\1=p' | sort >> found_by_git.txt } From 33af8146d71db3962195ff05354196cd819d6f9d Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 18:15:37 +0200 Subject: [PATCH 074/191] use current year and month --- scripts/find_labels.sh | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 85d67370e67c1d..c7119ae92ae868 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -35,7 +35,8 @@ git log --pretty=oneline --since="${startDate}" --until="${endDate}" | sed -n 's=.*\((#[0-9]*)\)$=\1=p' | sort >> found_by_git.txt } -yr_mth=2024-07 +# the current year and month +yr_mth="$(date +%Y-%m)" #2024-07 start_date="${yr_mth}-01T00:00:00" end_date="$(date -d "${yr_mth}-01 + 1 month - 1 day" +%Y-%m-%d)T23:59:59" From 3126e27282f88fecd4cd60b5725c9c3873d5a252 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 31 Jul 2024 20:15:09 +0200 Subject: [PATCH 075/191] split differently --- scripts/find_labels.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index c7119ae92ae868..83db7a46a22f04 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -45,8 +45,8 @@ commits_in_range="$(git log --since="${start_date}" --until="${end_date}" --pret printf $'\n%s commits between %s and %s\n' "${commits_in_range}" "${start_date}" "${end_date}" -findInRange "${1}" "${start_date}" "${yr_mth}-15T23:59:59" -findInRange "${1}" "${yr_mth}-16T00:00:00" "${end_date}" +findInRange "${1}" "${start_date}" "${yr_mth}-14T23:59:59" +findInRange "${1}" "${yr_mth}-15T00:00:00" "${end_date}" only_gh="$( comm -23 <(sort found_by_gh.txt) <(sort found_by_git.txt))" only_git="$(comm -13 <(sort found_by_gh.txt) <(sort found_by_git.txt))" From 48384c58bf6e2061663524a52878f53d2a9c3e30 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 10:29:40 +0200 Subject: [PATCH 076/191] print prs --- scripts/find_labels.sh | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 83db7a46a22f04..1ad96d8ed393c9 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -33,10 +33,12 @@ echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "(# # Store to file `found_by_git.txt` the PR numbers, as found by looking at the commits to `master` git log --pretty=oneline --since="${startDate}" --until="${endDate}" | sed -n 's=.*\((#[0-9]*)\)$=\1=p' | sort >> found_by_git.txt + +echo "$prs" } # the current year and month -yr_mth="$(date +%Y-%m)" #2024-07 +yr_mth=2024-07 #"$(date +%Y-%m)" start_date="${yr_mth}-01T00:00:00" end_date="$(date -d "${yr_mth}-01 + 1 month - 1 day" +%Y-%m-%d)T23:59:59" From ea56e8645b8ab34b5e48cd4103f5803abab09c11 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 11:41:25 +0200 Subject: [PATCH 077/191] filter better --- scripts/find_labels.sh | 52 ++++++++++++++++++++++++++++++++++++++---- 1 file changed, 48 insertions(+), 4 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 1ad96d8ed393c9..5c90f9a529184c 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -24,8 +24,8 @@ commits_in_range="$(git log --since="${startDate}" --until="${endDate}" --pretty # Retrieve merged PRs from the given range prs=$(gh pr list --repo "$repository" --state closed --base master --search "closed:${startDate}..${endDate}" --json number,labels,title --limit "$((commits_in_range * 2))") -# Print PR numbers, their labels and their title -echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Title: \(.title)"' +## Print PR numbers, their labels and their title +#echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Title: \(.title)"' # Store to file `found_by_gh.txt` the PR numbers, as found by `gh` echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "(#\(.number))"' | sort >> found_by_gh.txt @@ -37,6 +37,30 @@ git log --pretty=oneline --since="${startDate}" --until="${endDate}" | echo "$prs" } +#jq -S -r '.[] | +# select(.title | startswith("[Merged by Bors]")) | +# "\(.labels | map(.name | select(startswith("t-"))) // "No labels") PR #\(.number) \(.title)"' mwe_outputs/prBlog.txt | +# sort | +# awk 'BEGIN{ labels=""; con=0 } +# { if(!($1 in seen)) { con++; order[con]=$1; seen[$1]=0 } +# gsub(/\[Merged by Bors\] - /, "") +# rest=$2; for(i=3; i<=NF; i++){rest=rest" "$i};acc[$1]=acc[$1]"\n"rest } +# END { +# #for(lab in acc) { printf("%s%s\n", lab, acc[lab]) } +# for(i=1; i<=con; i++) { +# tag=order[i] +# gsub(/\[\]/, "Miscellaneous", tag) +# gsub(/[\"\][]/, "", tag) +# gsub(/,/, " ", tag) +# printf("\n%s: %s%s\n", i, tag, acc[order[i]]) +# } +# } +# ' + +#jq -r '.[] | +# select(.title | startswith("[Merged by Bors]")) | +# "Labels: \(.labels | map(.name) .[] // "No labels") (#\(.number))"' mwe_outputs/prBlog.txt + # the current year and month yr_mth=2024-07 #"$(date +%Y-%m)" @@ -47,8 +71,28 @@ commits_in_range="$(git log --since="${start_date}" --until="${end_date}" --pret printf $'\n%s commits between %s and %s\n' "${commits_in_range}" "${start_date}" "${end_date}" -findInRange "${1}" "${start_date}" "${yr_mth}-14T23:59:59" -findInRange "${1}" "${yr_mth}-15T00:00:00" "${end_date}" +( +findInRange "${1}" "${start_date}" "${yr_mth}-14T23:59:59" | sed -z 's=]\n*$=,\n=' +findInRange "${1}" "${yr_mth}-15T00:00:00" "${end_date}" | sed -z 's=^\[==' +) | jq -S -r '.[] | + select(.title | startswith("[Merged by Bors]")) | + "\(.labels | map(.name | select(startswith("t-"))) // "No labels") PR #\(.number) \(.title)"' | + sort | + awk 'BEGIN{ labels=""; con=0 } + { if(!($1 in seen)) { con++; order[con]=$1; seen[$1]=0 } + gsub(/\[Merged by Bors\] - /, "") + rest=$2; for(i=3; i<=NF; i++){rest=rest" "$i};acc[$1]=acc[$1]"\n"rest } + END { + #for(lab in acc) { printf("%s%s\n", lab, acc[lab]) } + for(i=1; i<=con; i++) { + tag=order[i] + gsub(/\[\]/, "Miscellaneous", tag) + gsub(/[\"\][]/, "", tag) + gsub(/,/, " ", tag) + printf("\n%s: %s%s\n", i, tag, acc[order[i]]) + } + } + ' only_gh="$( comm -23 <(sort found_by_gh.txt) <(sort found_by_git.txt))" only_git="$(comm -13 <(sort found_by_gh.txt) <(sort found_by_git.txt))" From 136093f83e03e8a2de7f464982e3c4a4959c8a8a Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 11:46:08 +0200 Subject: [PATCH 078/191] line breaks around reports --- scripts/find_labels.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 5c90f9a529184c..4513aa1b783e18 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -103,14 +103,14 @@ if [ -z "${only_gh}" ] then printf $'\n* All PRs are accounted for!\n' else - printf $'\n* PRs not corresponding to a commit\n\n%s\n' "${only_gh}" + printf $'\n* PRs not corresponding to a commit\n%s\n' "${only_gh}" fi if [ -z "${only_git}" ] then printf $'\n* All commits are accounted for!\n' else - printf $'* PRs not found by `gh`\n\n%s\n' "${only_git}" + printf $'\n* PRs not found by `gh`\n%s\n' "${only_git}" fi printf $'\n---\n' From 0716baa76ebae694843bfaaff23992c10a38acfa Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 11:49:13 +0200 Subject: [PATCH 079/191] omit unnecessary escaped double quote --- scripts/find_labels.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 4513aa1b783e18..58d041566f68e2 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -50,7 +50,7 @@ echo "$prs" # for(i=1; i<=con; i++) { # tag=order[i] # gsub(/\[\]/, "Miscellaneous", tag) -# gsub(/[\"\][]/, "", tag) +# gsub(/["\][]/, "", tag) # gsub(/,/, " ", tag) # printf("\n%s: %s%s\n", i, tag, acc[order[i]]) # } @@ -87,7 +87,7 @@ findInRange "${1}" "${yr_mth}-15T00:00:00" "${end_date}" | sed -z 's=^\[==' for(i=1; i<=con; i++) { tag=order[i] gsub(/\[\]/, "Miscellaneous", tag) - gsub(/[\"\][]/, "", tag) + gsub(/["\][]/, "", tag) gsub(/,/, " ", tag) printf("\n%s: %s%s\n", i, tag, acc[order[i]]) } From 088dda3ada46630f2f7d39bee8b9d1b665faacfd Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 13:18:30 +0200 Subject: [PATCH 080/191] clean up, add closed PR numbers --- scripts/find_labels.sh | 31 ++++--------------------------- 1 file changed, 4 insertions(+), 27 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 58d041566f68e2..5f9810fac04de3 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -37,30 +37,6 @@ git log --pretty=oneline --since="${startDate}" --until="${endDate}" | echo "$prs" } -#jq -S -r '.[] | -# select(.title | startswith("[Merged by Bors]")) | -# "\(.labels | map(.name | select(startswith("t-"))) // "No labels") PR #\(.number) \(.title)"' mwe_outputs/prBlog.txt | -# sort | -# awk 'BEGIN{ labels=""; con=0 } -# { if(!($1 in seen)) { con++; order[con]=$1; seen[$1]=0 } -# gsub(/\[Merged by Bors\] - /, "") -# rest=$2; for(i=3; i<=NF; i++){rest=rest" "$i};acc[$1]=acc[$1]"\n"rest } -# END { -# #for(lab in acc) { printf("%s%s\n", lab, acc[lab]) } -# for(i=1; i<=con; i++) { -# tag=order[i] -# gsub(/\[\]/, "Miscellaneous", tag) -# gsub(/["\][]/, "", tag) -# gsub(/,/, " ", tag) -# printf("\n%s: %s%s\n", i, tag, acc[order[i]]) -# } -# } -# ' - -#jq -r '.[] | -# select(.title | startswith("[Merged by Bors]")) | -# "Labels: \(.labels | map(.name) .[] // "No labels") (#\(.number))"' mwe_outputs/prBlog.txt - # the current year and month yr_mth=2024-07 #"$(date +%Y-%m)" @@ -78,12 +54,13 @@ findInRange "${1}" "${yr_mth}-15T00:00:00" "${end_date}" | sed -z 's=^\[==' select(.title | startswith("[Merged by Bors]")) | "\(.labels | map(.name | select(startswith("t-"))) // "No labels") PR #\(.number) \(.title)"' | sort | - awk 'BEGIN{ labels=""; con=0 } - { if(!($1 in seen)) { con++; order[con]=$1; seen[$1]=0 } + awk -v startDate="${start_date}" -v endDate="${end_date}" 'BEGIN{ labels=""; con=0; total=0 } + { total++ + if(!($1 in seen)) { con++; order[con]=$1; seen[$1]=0 } gsub(/\[Merged by Bors\] - /, "") rest=$2; for(i=3; i<=NF; i++){rest=rest" "$i};acc[$1]=acc[$1]"\n"rest } END { - #for(lab in acc) { printf("%s%s\n", lab, acc[lab]) } + printf("%s closed PRs between %s and %s\n\n", total, startDate, endDate) for(i=1; i<=con; i++) { tag=order[i] gsub(/\[\]/, "Miscellaneous", tag) From 20ca0daf74e08fbc24f03a5ca4138c7589efa9de Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 13:22:15 +0200 Subject: [PATCH 081/191] formatting --- scripts/find_labels.sh | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 5f9810fac04de3..74b24ec0125563 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -60,7 +60,7 @@ findInRange "${1}" "${yr_mth}-15T00:00:00" "${end_date}" | sed -z 's=^\[==' gsub(/\[Merged by Bors\] - /, "") rest=$2; for(i=3; i<=NF; i++){rest=rest" "$i};acc[$1]=acc[$1]"\n"rest } END { - printf("%s closed PRs between %s and %s\n\n", total, startDate, endDate) + printf("%s closed PRs between %s and %s\n", total, startDate, endDate) for(i=1; i<=con; i++) { tag=order[i] gsub(/\[\]/, "Miscellaneous", tag) @@ -78,9 +78,9 @@ printf $'\n---\nReports\n\n' if [ -z "${only_gh}" ] then - printf $'\n* All PRs are accounted for!\n' + printf $'* All PRs are accounted for!\n' else - printf $'\n* PRs not corresponding to a commit\n%s\n' "${only_gh}" + printf $'* PRs not corresponding to a commit\n%s\n' "${only_gh}" fi if [ -z "${only_git}" ] @@ -90,7 +90,7 @@ else printf $'\n* PRs not found by `gh`\n%s\n' "${only_git}" fi -printf $'\n---\n' +printf $'---\n' rm -rf found_by_gh.txt found_by_git.txt From 453aa581cf40b8e627d6f8ed6432fb77b1e01e3d Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 13:25:24 +0200 Subject: [PATCH 082/191] fix line break --- scripts/find_labels.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 74b24ec0125563..a67658e294c175 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -90,7 +90,7 @@ else printf $'\n* PRs not found by `gh`\n%s\n' "${only_git}" fi -printf $'---\n' +printf -- $'---\n' rm -rf found_by_gh.txt found_by_git.txt From 59711cf5193021036c9a7d5ef7761f22354703af Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 13:27:37 +0200 Subject: [PATCH 083/191] print date ranges once --- scripts/find_labels.sh | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index a67658e294c175..40f087badc392a 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -45,7 +45,9 @@ end_date="$(date -d "${yr_mth}-01 + 1 month - 1 day" +%Y-%m-%d)T23:59:59" commits_in_range="$(git log --since="${start_date}" --until="${end_date}" --pretty=oneline | wc -l)" -printf $'\n%s commits between %s and %s\n' "${commits_in_range}" "${start_date}" "${end_date}" +printf $'\nRange between %s and %s\n' "${start_date}" "${end_date}" + +printf $'\n%s commits to `master`\n' "${commits_in_range}" "${start_date}" "${end_date}" ( findInRange "${1}" "${start_date}" "${yr_mth}-14T23:59:59" | sed -z 's=]\n*$=,\n=' @@ -54,13 +56,13 @@ findInRange "${1}" "${yr_mth}-15T00:00:00" "${end_date}" | sed -z 's=^\[==' select(.title | startswith("[Merged by Bors]")) | "\(.labels | map(.name | select(startswith("t-"))) // "No labels") PR #\(.number) \(.title)"' | sort | - awk -v startDate="${start_date}" -v endDate="${end_date}" 'BEGIN{ labels=""; con=0; total=0 } + awk 'BEGIN{ labels=""; con=0; total=0 } { total++ if(!($1 in seen)) { con++; order[con]=$1; seen[$1]=0 } gsub(/\[Merged by Bors\] - /, "") rest=$2; for(i=3; i<=NF; i++){rest=rest" "$i};acc[$1]=acc[$1]"\n"rest } END { - printf("%s closed PRs between %s and %s\n", total, startDate, endDate) + printf("%s closed PRs\n", total) for(i=1; i<=con; i++) { tag=order[i] gsub(/\[\]/, "Miscellaneous", tag) From 50a23e700e18c91b91cb5afff7680cd2437465b8 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 13:31:08 +0200 Subject: [PATCH 084/191] formatting --- scripts/find_labels.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 40f087badc392a..a05917e5dfbb58 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -45,9 +45,9 @@ end_date="$(date -d "${yr_mth}-01 + 1 month - 1 day" +%Y-%m-%d)T23:59:59" commits_in_range="$(git log --since="${start_date}" --until="${end_date}" --pretty=oneline | wc -l)" -printf $'\nRange between %s and %s\n' "${start_date}" "${end_date}" +printf $'\nBetween %s and %s there were\n' "${start_date/%T*}" "${end_date/%T*}" -printf $'\n%s commits to `master`\n' "${commits_in_range}" "${start_date}" "${end_date}" +printf $'%s commits to `master`\n' "${commits_in_range}" ( findInRange "${1}" "${start_date}" "${yr_mth}-14T23:59:59" | sed -z 's=]\n*$=,\n=' From da0203e49239668a09fa0f0f9f7c9e8d844e2168 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 13:33:39 +0200 Subject: [PATCH 085/191] stars --- scripts/find_labels.sh | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index a05917e5dfbb58..1df0de46ac0009 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -45,9 +45,9 @@ end_date="$(date -d "${yr_mth}-01 + 1 month - 1 day" +%Y-%m-%d)T23:59:59" commits_in_range="$(git log --since="${start_date}" --until="${end_date}" --pretty=oneline | wc -l)" -printf $'\nBetween %s and %s there were\n' "${start_date/%T*}" "${end_date/%T*}" +printf $'\n\nBetween %s and %s there were\n' "${start_date/%T*}" "${end_date/%T*}" -printf $'%s commits to `master`\n' "${commits_in_range}" +printf $'* %s commits to `master` and\n' "${commits_in_range}" ( findInRange "${1}" "${start_date}" "${yr_mth}-14T23:59:59" | sed -z 's=]\n*$=,\n=' @@ -62,7 +62,7 @@ findInRange "${1}" "${yr_mth}-15T00:00:00" "${end_date}" | sed -z 's=^\[==' gsub(/\[Merged by Bors\] - /, "") rest=$2; for(i=3; i<=NF; i++){rest=rest" "$i};acc[$1]=acc[$1]"\n"rest } END { - printf("%s closed PRs\n", total) + printf("* %s closed PRs\n", total) for(i=1; i<=con; i++) { tag=order[i] gsub(/\[\]/, "Miscellaneous", tag) From 9ed2e09eb7a19de3deffa588948e7bd07c79cc73 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 13:43:23 +0200 Subject: [PATCH 086/191] months --- scripts/find_labels.sh | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 1df0de46ac0009..d4ced9d8aefdc1 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -78,11 +78,14 @@ only_git="$(comm -13 <(sort found_by_gh.txt) <(sort found_by_git.txt))" printf $'\n---\nReports\n\n' +mth="$(date -d "${yr_mth}-01" '+%b')" +prev_mth="$(date -d "${yr_mth}-01 - 1 day" '+%b')" + if [ -z "${only_gh}" ] then printf $'* All PRs are accounted for!\n' else - printf $'* PRs not corresponding to a commit\n%s\n' "${only_gh}" + printf $'* PRs not corresponding to a commit (closed in %s, merged in %s)\n%s\n' "${mth}" "${prev_mth}" "${only_gh}" fi if [ -z "${only_git}" ] From be8a01f0a96c80e42f188b9a7b623f59fa99a6d9 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 13:46:38 +0200 Subject: [PATCH 087/191] next month --- scripts/find_labels.sh | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index d4ced9d8aefdc1..d0682336d2d47e 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -78,21 +78,22 @@ only_git="$(comm -13 <(sort found_by_gh.txt) <(sort found_by_git.txt))" printf $'\n---\nReports\n\n' -mth="$(date -d "${yr_mth}-01" '+%b')" -prev_mth="$(date -d "${yr_mth}-01 - 1 day" '+%b')" +mth="$(date -d "${yr_mth}-01" '+%B')" +prev_mth="$(date -d "${yr_mth}-01 - 1 day" '+%B')" +next_mth="$(date -d "${yr_mth}-01 + 1 month" '+%B')" if [ -z "${only_gh}" ] then printf $'* All PRs are accounted for!\n' else - printf $'* PRs not corresponding to a commit (closed in %s, merged in %s)\n%s\n' "${mth}" "${prev_mth}" "${only_gh}" + printf $'* PRs not corresponding to a commit (merged in %s, closed in %s)\n%s\n' "${prev_mth}" "${mth}" "${only_gh}" fi if [ -z "${only_git}" ] then printf $'\n* All commits are accounted for!\n' else - printf $'\n* PRs not found by `gh`\n%s\n' "${only_git}" + printf $'\n* PRs not found by `gh` (merged in %s, closed in %s)\n%s\n' "${mth}" "${next_mth}" "${only_git}" fi printf -- $'---\n' From 6f0e59ba8ea0800385140a9e4fce7e2afff15e44 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 14:00:00 +0200 Subject: [PATCH 088/191] pad exceptions, remove parens --- scripts/find_labels.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index d0682336d2d47e..2ea8159a28ec02 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -73,8 +73,8 @@ findInRange "${1}" "${yr_mth}-15T00:00:00" "${end_date}" | sed -z 's=^\[==' } ' -only_gh="$( comm -23 <(sort found_by_gh.txt) <(sort found_by_git.txt))" -only_git="$(comm -13 <(sort found_by_gh.txt) <(sort found_by_git.txt))" +only_gh="$( comm -23 <(sort found_by_gh.txt) <(sort found_by_git.txt) | sed 's=^= =' | tr -d '()')" +only_git="$(comm -13 <(sort found_by_gh.txt) <(sort found_by_git.txt) | sed 's=^= =' | tr -d '()')" printf $'\n---\nReports\n\n' From 7e51b995d5387bd1ba264c4440fa523fbb266986 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 14:08:39 +0200 Subject: [PATCH 089/191] Add question marks --- scripts/find_labels.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 2ea8159a28ec02..05aea42ca5e5b9 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -86,14 +86,14 @@ if [ -z "${only_gh}" ] then printf $'* All PRs are accounted for!\n' else - printf $'* PRs not corresponding to a commit (merged in %s, closed in %s)\n%s\n' "${prev_mth}" "${mth}" "${only_gh}" + printf $'* PRs not corresponding to a commit (merged in %s, closed in %s?)\n%s\n' "${prev_mth}" "${mth}" "${only_gh}" fi if [ -z "${only_git}" ] then printf $'\n* All commits are accounted for!\n' else - printf $'\n* PRs not found by `gh` (merged in %s, closed in %s)\n%s\n' "${mth}" "${next_mth}" "${only_git}" + printf $'\n* PRs not found by `gh` (merged in %s, closed in %s?)\n%s\n' "${mth}" "${next_mth}" "${only_git}" fi printf -- $'---\n' From a2f1a2fcd5a50351a95631124e9054ac61351364 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 14:13:29 +0200 Subject: [PATCH 090/191] dates go up --- scripts/find_labels.sh | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 05aea42ca5e5b9..cd92b0ff044bd0 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -39,9 +39,14 @@ echo "$prs" # the current year and month yr_mth=2024-07 #"$(date +%Y-%m)" +yr_mth_day=2024-07-01 -start_date="${yr_mth}-01T00:00:00" -end_date="$(date -d "${yr_mth}-01 + 1 month - 1 day" +%Y-%m-%d)T23:59:59" +start_date="${yr_mth_day}T00:00:00" +end_date="$(date -d "${yr_mth_day} + 1 month - 1 day" +%Y-%m-%d)T23:59:59" + +mth="$(date -d "${yr_mth_day}" '+%B')" +prev_mth="$(date -d "${yr_mth_day} - 1 day" '+%B')" +next_mth="$(date -d "${yr_mth_day} + 1 month" '+%B')" commits_in_range="$(git log --since="${start_date}" --until="${end_date}" --pretty=oneline | wc -l)" @@ -78,10 +83,6 @@ only_git="$(comm -13 <(sort found_by_gh.txt) <(sort found_by_git.txt) | sed 's=^ printf $'\n---\nReports\n\n' -mth="$(date -d "${yr_mth}-01" '+%B')" -prev_mth="$(date -d "${yr_mth}-01 - 1 day" '+%B')" -next_mth="$(date -d "${yr_mth}-01 + 1 month" '+%B')" - if [ -z "${only_gh}" ] then printf $'* All PRs are accounted for!\n' From 93cf6c638311add3881f0f4ace5a937cec860ba5 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 14:15:56 +0200 Subject: [PATCH 091/191] 14 15 16 --- scripts/find_labels.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index cd92b0ff044bd0..1e39169979c180 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -55,8 +55,8 @@ printf $'\n\nBetween %s and %s there were\n' "${start_date/%T*}" "${end_date/%T* printf $'* %s commits to `master` and\n' "${commits_in_range}" ( -findInRange "${1}" "${start_date}" "${yr_mth}-14T23:59:59" | sed -z 's=]\n*$=,\n=' -findInRange "${1}" "${yr_mth}-15T00:00:00" "${end_date}" | sed -z 's=^\[==' +findInRange "${1}" "${start_date}" "${yr_mth}-15T23:59:59" | sed -z 's=]\n*$=,\n=' +findInRange "${1}" "${yr_mth}-16T00:00:00" "${end_date}" | sed -z 's=^\[==' ) | jq -S -r '.[] | select(.title | startswith("[Merged by Bors]")) | "\(.labels | map(.name | select(startswith("t-"))) // "No labels") PR #\(.number) \(.title)"' | From f2143bd234d2aaee7ee4cb7a76ad9bc577863672 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 14:16:51 +0200 Subject: [PATCH 092/191] recycle --- scripts/find_labels.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 1e39169979c180..af3a6a0f6e374e 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -50,7 +50,7 @@ next_mth="$(date -d "${yr_mth_day} + 1 month" '+%B')" commits_in_range="$(git log --since="${start_date}" --until="${end_date}" --pretty=oneline | wc -l)" -printf $'\n\nBetween %s and %s there were\n' "${start_date/%T*}" "${end_date/%T*}" +printf $'\n\nBetween %s and %s there were\n' "${yr_mth_day}" "${end_date/%T*}" printf $'* %s commits to `master` and\n' "${commits_in_range}" From 63f9835a4da313b2ae4693f574c4a6a0b27fca06 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 17:37:14 +0200 Subject: [PATCH 093/191] add authors --- scripts/find_labels.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index af3a6a0f6e374e..7f73b570a4c9a9 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -22,7 +22,7 @@ endDate="${3}" commits_in_range="$(git log --since="${startDate}" --until="${endDate}" --pretty=oneline | wc -l)" # Retrieve merged PRs from the given range -prs=$(gh pr list --repo "$repository" --state closed --base master --search "closed:${startDate}..${endDate}" --json number,labels,title --limit "$((commits_in_range * 2))") +prs=$(gh pr list --repo "$repository" --state closed --base master --search "closed:${startDate}..${endDate}" --json number,labels,title,authors --limit "$((commits_in_range * 2))") ## Print PR numbers, their labels and their title #echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Title: \(.title)"' From 6ec7878dbb09db69f7e2a3cba5ccda5dbc2ddc9b Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 17:37:23 +0200 Subject: [PATCH 094/191] new workflow --- .github/workflows/monthly_pr_report.yaml | 32 ++++++++++++++++++++++++ 1 file changed, 32 insertions(+) create mode 100644 .github/workflows/monthly_pr_report.yaml diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml new file mode 100644 index 00000000000000..654888733c1e15 --- /dev/null +++ b/.github/workflows/monthly_pr_report.yaml @@ -0,0 +1,32 @@ + +on: + pull_request + +name: Blog report + +jobs: + + style_lint: + if: github.repository == 'leanprover-community/mathlib4' && github.event.pull_request.draft == false + name: Blog draft + runs-on: ubuntu-latest + + env: + GH_TOKEN: ${{ github.token }} + BRANCH_NAME: ${{ github.head_ref }} + + steps: + - name: cleanup + run: | + find . -name . -o -prune -exec rm -rf -- {} + + + - uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: master + + - name: blog report + continue-on-error: true + run: | + printf $'Repository: %s\nBranch: %s\n' "${{ github.repository }}" "${BRANCH_NAME}" + ./scripts/find_labels.sh "${{ github.repository }}" From a8a3b72ec1dd7ed9389718a4ec092a0143d4ae13 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 17:39:18 +0200 Subject: [PATCH 095/191] add author --- scripts/find_labels.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 7f73b570a4c9a9..bf7ebd9c0e4ce3 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -22,7 +22,7 @@ endDate="${3}" commits_in_range="$(git log --since="${startDate}" --until="${endDate}" --pretty=oneline | wc -l)" # Retrieve merged PRs from the given range -prs=$(gh pr list --repo "$repository" --state closed --base master --search "closed:${startDate}..${endDate}" --json number,labels,title,authors --limit "$((commits_in_range * 2))") +prs=$(gh pr list --repo "$repository" --state closed --base master --search "closed:${startDate}..${endDate}" --json number,labels,title,author --limit "$((commits_in_range * 2))") ## Print PR numbers, their labels and their title #echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Title: \(.title)"' From 3c49769199e3ce36ae210c74fe0275d43e2daed8 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 17:41:17 +0200 Subject: [PATCH 096/191] ls --- .github/workflows/monthly_pr_report.yaml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 654888733c1e15..c26373eeef79e7 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -29,4 +29,5 @@ jobs: continue-on-error: true run: | printf $'Repository: %s\nBranch: %s\n' "${{ github.repository }}" "${BRANCH_NAME}" + ls ./scripts/find_labels.sh "${{ github.repository }}" From edf76ebdb156f7af84ddac09fa89c3f58c36bef9 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 17:43:52 +0200 Subject: [PATCH 097/191] checkout the right file --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index c26373eeef79e7..d4296008859747 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -29,5 +29,5 @@ jobs: continue-on-error: true run: | printf $'Repository: %s\nBranch: %s\n' "${{ github.repository }}" "${BRANCH_NAME}" - ls + git checkout adomani/yd_find_label scripts/find_labels.sh ./scripts/find_labels.sh "${{ github.repository }}" From e122bc7c76195b0e3541c0781fb27035a2040fe0 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 17:46:22 +0200 Subject: [PATCH 098/191] checkout origin --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index d4296008859747..5c8c958f0f96c5 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -29,5 +29,5 @@ jobs: continue-on-error: true run: | printf $'Repository: %s\nBranch: %s\n' "${{ github.repository }}" "${BRANCH_NAME}" - git checkout adomani/yd_find_label scripts/find_labels.sh + git checkout origin/adomani/yd_find_label scripts/find_labels.sh ./scripts/find_labels.sh "${{ github.repository }}" From 9702a0dd806bc782dc3bf702f1b1f6ee83e3ef45 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 17:51:25 +0200 Subject: [PATCH 099/191] clean up after new action --- .github/workflows/lint_and_suggest_pr.yml | 18 ++---------------- scripts/find_labels.sh | 4 ---- 2 files changed, 2 insertions(+), 20 deletions(-) diff --git a/.github/workflows/lint_and_suggest_pr.yml b/.github/workflows/lint_and_suggest_pr.yml index e46186292a645c..64f06540402cd3 100644 --- a/.github/workflows/lint_and_suggest_pr.yml +++ b/.github/workflows/lint_and_suggest_pr.yml @@ -5,21 +5,17 @@ on: name: lint and suggest jobs: - style_lint: if: github.repository == 'leanprover-community/mathlib4' && github.event.pull_request.draft == false name: Lint style runs-on: ubuntu-latest - - env: - GH_TOKEN: ${{ github.token }} - BRANCH_NAME: ${{ github.head_ref }} - steps: - name: cleanup run: | find . -name . -o -prune -exec rm -rf -- {} + + - uses: actions/checkout@v4 + - name: install Python uses: actions/setup-python@v4 with: @@ -32,16 +28,6 @@ jobs: ./elan-init -y --default-toolchain none echo "$HOME/.elan/bin" >> "${GITHUB_PATH}" - - uses: actions/checkout@v4 - with: - fetch-depth: 0 - - - name: blog report - continue-on-error: true - run: | - printf $'Repository: %s\nBranch: %s\n' "${{ github.repository }}" "${BRANCH_NAME}" - ./scripts/find_labels.sh "${{ github.repository }}" - - name: lint continue-on-error: true # allows the following `reviewdog` step to add GitHub suggestions run: | diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index bf7ebd9c0e4ce3..f937079e4e796f 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -6,8 +6,6 @@ if [ "$#" -ne 1 ]; then exit 1 fi -git switch master - rm -rf found_by_gh.txt found_by_git.txt findInRange () { @@ -100,5 +98,3 @@ fi printf -- $'---\n' rm -rf found_by_gh.txt found_by_git.txt - -git checkout - From 7f7c1ac3bffb1ecf93cae5289fdb5e0f488a641a Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 17:56:09 +0200 Subject: [PATCH 100/191] print with authors --- scripts/find_labels.sh | 2 ++ 1 file changed, 2 insertions(+) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index f937079e4e796f..0cf936364366de 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -98,3 +98,5 @@ fi printf -- $'---\n' rm -rf found_by_gh.txt found_by_git.txt + +prs=$(gh pr list --repo "$repository" --state closed --base master --search "closed:${startDate}..${endDate}" --json number,labels,title,author --limit "$((commits_in_range * 2))") From eb5ea7fda63f3a958e6a1eca6b01ec034622211e Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 17:58:21 +0200 Subject: [PATCH 101/191] really print --- scripts/find_labels.sh | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 0cf936364366de..9428c3fc136fbb 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -99,4 +99,10 @@ printf -- $'---\n' rm -rf found_by_gh.txt found_by_git.txt -prs=$(gh pr list --repo "$repository" --state closed --base master --search "closed:${startDate}..${endDate}" --json number,labels,title,author --limit "$((commits_in_range * 2))") +gh pr list + --repo "$repository" + --state closed + --base master + --search "closed:${startDate}..${endDate}" + --json number,labels,title,author + --limit "$((commits_in_range * 2))" From e96c6498faf9a011f01879e10c60fc76b3406bf0 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 17:59:56 +0200 Subject: [PATCH 102/191] single line --- scripts/find_labels.sh | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 9428c3fc136fbb..04ec6488540187 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -99,10 +99,4 @@ printf -- $'---\n' rm -rf found_by_gh.txt found_by_git.txt -gh pr list - --repo "$repository" - --state closed - --base master - --search "closed:${startDate}..${endDate}" - --json number,labels,title,author - --limit "$((commits_in_range * 2))" +gh pr list --repo "$repository" --state closed --base master --search "closed:${startDate}..${endDate}" --json number,labels,title,author --limit "$((commits_in_range * 2))" From 30d5331af17bcb8f4190eda0e29bca63575fac6d Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 18:02:17 +0200 Subject: [PATCH 103/191] start/end _date --- scripts/find_labels.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 04ec6488540187..d4f6f3557933d4 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -99,4 +99,4 @@ printf -- $'---\n' rm -rf found_by_gh.txt found_by_git.txt -gh pr list --repo "$repository" --state closed --base master --search "closed:${startDate}..${endDate}" --json number,labels,title,author --limit "$((commits_in_range * 2))" +gh pr list --repo "$repository" --state closed --base master --search "closed:${start_date}..${end_date}" --json number,labels,title,author --limit "$((commits_in_range * 2))" From f6a6e0cc9bcec3a0544219d59c9efc87427cd7e3 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 18:26:47 +0200 Subject: [PATCH 104/191] add author name --- scripts/find_labels.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index d4f6f3557933d4..8a2b3af2cca900 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -57,7 +57,7 @@ findInRange "${1}" "${start_date}" "${yr_mth}-15T23:59:59" | sed -z 's=]\n*$=,\n findInRange "${1}" "${yr_mth}-16T00:00:00" "${end_date}" | sed -z 's=^\[==' ) | jq -S -r '.[] | select(.title | startswith("[Merged by Bors]")) | - "\(.labels | map(.name | select(startswith("t-"))) // "No labels") PR #\(.number) \(.title)"' | + "\(.labels | map(.name | select(startswith("t-"))) // "No labels") Author: \(if .author.name == "" then .author.login else .author.name end) PR #\(.number) \(.title)"' | sort | awk 'BEGIN{ labels=""; con=0; total=0 } { total++ From de359dcc0cf7cd38f944cf2d033f87663e987624 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 18:27:28 +0200 Subject: [PATCH 105/191] do not print the json --- scripts/find_labels.sh | 2 -- 1 file changed, 2 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 8a2b3af2cca900..65428806dcfaee 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -98,5 +98,3 @@ fi printf -- $'---\n' rm -rf found_by_gh.txt found_by_git.txt - -gh pr list --repo "$repository" --state closed --base master --search "closed:${start_date}..${end_date}" --json number,labels,title,author --limit "$((commits_in_range * 2))" From 74bdcadbe3ace46f000a2866584e827d7c877594 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 18:31:18 +0200 Subject: [PATCH 106/191] remove "or null" --- scripts/find_labels.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 65428806dcfaee..3d19a4b96b16d6 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -57,7 +57,7 @@ findInRange "${1}" "${start_date}" "${yr_mth}-15T23:59:59" | sed -z 's=]\n*$=,\n findInRange "${1}" "${yr_mth}-16T00:00:00" "${end_date}" | sed -z 's=^\[==' ) | jq -S -r '.[] | select(.title | startswith("[Merged by Bors]")) | - "\(.labels | map(.name | select(startswith("t-"))) // "No labels") Author: \(if .author.name == "" then .author.login else .author.name end) PR #\(.number) \(.title)"' | + "\(.labels | map(.name | select(startswith("t-"))) ) Author: \(if .author.name == "" then .author.login else .author.name end) PR #\(.number) \(.title)"' | sort | awk 'BEGIN{ labels=""; con=0; total=0 } { total++ From 5b378200f27364d7dda680e92a4f96746b9da541 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 18:33:17 +0200 Subject: [PATCH 107/191] PR number before author --- scripts/find_labels.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 3d19a4b96b16d6..3703c0da97a73f 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -57,7 +57,7 @@ findInRange "${1}" "${start_date}" "${yr_mth}-15T23:59:59" | sed -z 's=]\n*$=,\n findInRange "${1}" "${yr_mth}-16T00:00:00" "${end_date}" | sed -z 's=^\[==' ) | jq -S -r '.[] | select(.title | startswith("[Merged by Bors]")) | - "\(.labels | map(.name | select(startswith("t-"))) ) Author: \(if .author.name == "" then .author.login else .author.name end) PR #\(.number) \(.title)"' | + "\(.labels | map(.name | select(startswith("t-"))) ) PR #\(.number) Author: \(if .author.name == "" then .author.login else .author.name end) \(.title)"' | sort | awk 'BEGIN{ labels=""; con=0; total=0 } { total++ From d931fef7e6e2631aff58be27a20b1ab7e1cb9043 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 18:39:46 +0200 Subject: [PATCH 108/191] rename job --- .github/workflows/monthly_pr_report.yaml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 5c8c958f0f96c5..55b930a2c56291 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -1,4 +1,3 @@ - on: pull_request @@ -6,7 +5,7 @@ name: Blog report jobs: - style_lint: + Monthly_PRs: if: github.repository == 'leanprover-community/mathlib4' && github.event.pull_request.draft == false name: Blog draft runs-on: ubuntu-latest From 4da1164e746c66878bb2a3ba556d890b4b450936 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 19:22:49 +0200 Subject: [PATCH 109/191] reformat --- scripts/find_labels.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 3703c0da97a73f..1fd1eb423b9f60 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -57,7 +57,7 @@ findInRange "${1}" "${start_date}" "${yr_mth}-15T23:59:59" | sed -z 's=]\n*$=,\n findInRange "${1}" "${yr_mth}-16T00:00:00" "${end_date}" | sed -z 's=^\[==' ) | jq -S -r '.[] | select(.title | startswith("[Merged by Bors]")) | - "\(.labels | map(.name | select(startswith("t-"))) ) PR #\(.number) Author: \(if .author.name == "" then .author.login else .author.name end) \(.title)"' | + "\(.labels | map(.name | select(startswith("t-"))) ) PR #\(.number) \(if .author.name == "" then .author.login else .author.name end): \(.title)"' | sort | awk 'BEGIN{ labels=""; con=0; total=0 } { total++ From 9cf2cb195850f65fdb0cb11301387c1b7ce76722 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 19:35:54 +0200 Subject: [PATCH 110/191] print seen --- scripts/find_labels.sh | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 1fd1eb423b9f60..12d22c78fe82a7 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -61,7 +61,8 @@ findInRange "${1}" "${yr_mth}-16T00:00:00" "${end_date}" | sed -z 's=^\[==' sort | awk 'BEGIN{ labels=""; con=0; total=0 } { total++ - if(!($1 in seen)) { con++; order[con]=$1; seen[$1]=0 } + if(!($1 in seen)) { con++; order[con]=$1 } + seen[$1]++ gsub(/\[Merged by Bors\] - /, "") rest=$2; for(i=3; i<=NF; i++){rest=rest" "$i};acc[$1]=acc[$1]"\n"rest } END { @@ -71,7 +72,7 @@ findInRange "${1}" "${yr_mth}-16T00:00:00" "${end_date}" | sed -z 's=^\[==' gsub(/\[\]/, "Miscellaneous", tag) gsub(/["\][]/, "", tag) gsub(/,/, " ", tag) - printf("\n%s: %s%s\n", i, tag, acc[order[i]]) + printf("\n%s: %s%s\n", seen[i], tag, acc[order[i]]) } } ' From 0888ad4cf978214e907fe0a0cd9e0469dbbfd62b Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 19:38:44 +0200 Subject: [PATCH 111/191] initialize seen, use seen[order[i]] --- scripts/find_labels.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 12d22c78fe82a7..16ff078873d3cd 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -61,7 +61,7 @@ findInRange "${1}" "${yr_mth}-16T00:00:00" "${end_date}" | sed -z 's=^\[==' sort | awk 'BEGIN{ labels=""; con=0; total=0 } { total++ - if(!($1 in seen)) { con++; order[con]=$1 } + if(!($1 in seen)) { con++; order[con]=$1; seen[$1]=0 } seen[$1]++ gsub(/\[Merged by Bors\] - /, "") rest=$2; for(i=3; i<=NF; i++){rest=rest" "$i};acc[$1]=acc[$1]"\n"rest } @@ -72,7 +72,7 @@ findInRange "${1}" "${yr_mth}-16T00:00:00" "${end_date}" | sed -z 's=^\[==' gsub(/\[\]/, "Miscellaneous", tag) gsub(/["\][]/, "", tag) gsub(/,/, " ", tag) - printf("\n%s: %s%s\n", seen[i], tag, acc[order[i]]) + printf("\n%s: %s%s\n", seen[order[i]], tag, acc[order[i]]) } } ' From 23744bd7c078d16fe94bb7b21997e69f5534dbbc Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 19:41:09 +0200 Subject: [PATCH 112/191] header --- scripts/find_labels.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 16ff078873d3cd..31d29c88e0ac1c 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -72,7 +72,7 @@ findInRange "${1}" "${yr_mth}-16T00:00:00" "${end_date}" | sed -z 's=^\[==' gsub(/\[\]/, "Miscellaneous", tag) gsub(/["\][]/, "", tag) gsub(/,/, " ", tag) - printf("\n%s: %s%s\n", seen[order[i]], tag, acc[order[i]]) + printf("\n%s, %s PRs%s\n", tag, seen[order[i]], acc[order[i]]) } } ' From 923dc2d7b164b5017f8e8d231276f48b506a7901 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 19:47:02 +0200 Subject: [PATCH 113/191] maintain a comment --- .github/workflows/monthly_pr_report.yaml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 55b930a2c56291..10c4719d9badbe 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -27,6 +27,12 @@ jobs: - name: blog report continue-on-error: true run: | + PR="${{ github.event.pull_request.number }}" + title="### Month in Mathlib summary" + printf $'Repository: %s\nBranch: %s\n' "${{ github.repository }}" "${BRANCH_NAME}" git checkout origin/adomani/yd_find_label scripts/find_labels.sh - ./scripts/find_labels.sh "${{ github.repository }}" + message="$(./scripts/find_labels.sh "${{ github.repository }}")" + echo "${message}" + + ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" From 4ded3a4c4b38bb6da4fac9e5c5a12bb91c2b7959 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 19:51:06 +0200 Subject: [PATCH 114/191] embed title in message --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 10c4719d9badbe..2a17819cc74bc6 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -32,7 +32,7 @@ jobs: printf $'Repository: %s\nBranch: %s\n' "${{ github.repository }}" "${BRANCH_NAME}" git checkout origin/adomani/yd_find_label scripts/find_labels.sh - message="$(./scripts/find_labels.sh "${{ github.repository }}")" + message="${title}\n$(./scripts/find_labels.sh "${{ github.repository }}")" echo "${message}" ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" From 7e39374d67d199aadba3fa98085257b9a48f6f58 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 19:56:44 +0200 Subject: [PATCH 115/191] printf --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 2a17819cc74bc6..3442cdd642e5a0 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -32,7 +32,7 @@ jobs: printf $'Repository: %s\nBranch: %s\n' "${{ github.repository }}" "${BRANCH_NAME}" git checkout origin/adomani/yd_find_label scripts/find_labels.sh - message="${title}\n$(./scripts/find_labels.sh "${{ github.repository }}")" + message="$(printf '%s\n\n%s\n' "${title}" "$(./scripts/find_labels.sh "${{ github.repository }}")")" echo "${message}" ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" From c097f4d2eef02fabb1dc55b1a5e69180469e9f72 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 19:59:57 +0200 Subject: [PATCH 116/191] use secrets --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 3442cdd642e5a0..870ec927e016bb 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -11,7 +11,7 @@ jobs: runs-on: ubuntu-latest env: - GH_TOKEN: ${{ github.token }} + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} BRANCH_NAME: ${{ github.head_ref }} steps: From 8cc618d18aeaf430f0fd16792172f7c22855a23c Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 22:10:08 +0200 Subject: [PATCH 117/191] some formatting --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 870ec927e016bb..e3605394c91bee 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -35,4 +35,4 @@ jobs: message="$(printf '%s\n\n%s\n' "${title}" "$(./scripts/find_labels.sh "${{ github.repository }}")")" echo "${message}" - ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" + ./scripts/update_PR_comment.sh "$(echo ${message} | sed '/ [0-9]* PRs$/{s=^=
\n\n\n=; s=$=\n\n=}' mwe_outputs/prBlog.md)" "${title}" "${PR}" From 0ae1677651003a4d2e19d0483f052bf29c63214e Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 22:11:23 +0200 Subject: [PATCH 118/191] quotes --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index e3605394c91bee..f88c8a170f162b 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -35,4 +35,4 @@ jobs: message="$(printf '%s\n\n%s\n' "${title}" "$(./scripts/find_labels.sh "${{ github.repository }}")")" echo "${message}" - ./scripts/update_PR_comment.sh "$(echo ${message} | sed '/ [0-9]* PRs$/{s=^=
\n\n\n=; s=$=\n\n=}' mwe_outputs/prBlog.md)" "${title}" "${PR}" + ./scripts/update_PR_comment.sh "$(echo "${message}" | sed '/ [0-9]* PRs$/{s=^=
\n\n\n=; s=$=\n\n=}' mwe_outputs/prBlog.md)" "${title}" "${PR}" From 8fedb6e0f5ebf1c499450cae8884b4e431ca3b11 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 22:13:01 +0200 Subject: [PATCH 119/191] end --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index f88c8a170f162b..9ba1bcb56e476a 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -35,4 +35,4 @@ jobs: message="$(printf '%s\n\n%s\n' "${title}" "$(./scripts/find_labels.sh "${{ github.repository }}")")" echo "${message}" - ./scripts/update_PR_comment.sh "$(echo "${message}" | sed '/ [0-9]* PRs$/{s=^=
\n\n\n=; s=$=\n\n=}' mwe_outputs/prBlog.md)" "${title}" "${PR}" + ./scripts/update_PR_comment.sh "$(echo "${message}" | sed '/ [0-9]* PRs$/{s=^=
\n\n\n=; s=$=\n\n=} | sed -z 's=\n---\nReports\n\n=\n&='' mwe_outputs/prBlog.md)" "${title}" "${PR}" From da8605fd340f01f43979f51ecaa6e184a5eff6c4 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 22:14:43 +0200 Subject: [PATCH 120/191] remove filename --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 9ba1bcb56e476a..727d6566eddfb6 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -35,4 +35,4 @@ jobs: message="$(printf '%s\n\n%s\n' "${title}" "$(./scripts/find_labels.sh "${{ github.repository }}")")" echo "${message}" - ./scripts/update_PR_comment.sh "$(echo "${message}" | sed '/ [0-9]* PRs$/{s=^=
\n\n\n=; s=$=\n\n=} | sed -z 's=\n---\nReports\n\n=\n&='' mwe_outputs/prBlog.md)" "${title}" "${PR}" + ./scripts/update_PR_comment.sh "$(echo "${message}" | sed '/ [0-9]* PRs$/{s=^=
\n\n\n=; s=$=\n\n=} | sed -z 's=\n---\nReports\n\n=\n&='')" "${title}" "${PR}" From ed4c19038d78286c2972f36bb5bd73f253636d1e Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 22:17:43 +0200 Subject: [PATCH 121/191] ticks --- .github/workflows/monthly_pr_report.yaml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 727d6566eddfb6..109bbc5c5830d2 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -34,5 +34,9 @@ jobs: git checkout origin/adomani/yd_find_label scripts/find_labels.sh message="$(printf '%s\n\n%s\n' "${title}" "$(./scripts/find_labels.sh "${{ github.repository }}")")" echo "${message}" - - ./scripts/update_PR_comment.sh "$(echo "${message}" | sed '/ [0-9]* PRs$/{s=^=
\n\n\n=; s=$=\n\n=} | sed -z 's=\n---\nReports\n\n=\n&='')" "${title}" "${PR}" + message="$(echo "${message}" | + sed '/ [0-9]* PRs$/{ + s=^=
\n\n\n= + s=$=\n\n= + }' | sed -z 's=\n---\nReports\n\n=\n&=')" + ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" From 2eb5998ad3f55764c437ea641f73de71d60fe522 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 22:19:40 +0200 Subject: [PATCH 122/191] line break --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 109bbc5c5830d2..c53b60f829c0b8 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -38,5 +38,5 @@ jobs: sed '/ [0-9]* PRs$/{ s=^=
\n\n\n= s=$=\n\n= - }' | sed -z 's=\n---\nReports\n\n=\n&=')" + }' | sed -z 's=\n---\nReports\n\n=\n\n&=')" ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" From 0a9b684b9dcffd2a5f84317161ad444077ea3421 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 22:21:56 +0200 Subject: [PATCH 123/191] close details --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index c53b60f829c0b8..a7efec83799068 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -38,5 +38,5 @@ jobs: sed '/ [0-9]* PRs$/{ s=^=
\n\n\n= s=$=\n\n= - }' | sed -z 's=\n---\nReports\n\n=\n\n&=')" + }' | sed -z 's=\n---\nReports\n\n=\n
\n&=')" ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" From f3d0a0989be6e2b6f8b6aaf744809724fb4a1c90 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 22:22:59 +0200 Subject: [PATCH 124/191] remove initial PR --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index a7efec83799068..4816be31e8ba5d 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -38,5 +38,5 @@ jobs: sed '/ [0-9]* PRs$/{ s=^=
\n\n\n= s=$=\n\n= - }' | sed -z 's=\n---\nReports\n\n=\n
\n&=')" + }; s=^PR ==' | sed -z 's=\n---\nReports\n\n=\n\n&=')" ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" From d4974a6d4e1a77856b2525519b2aa6b6fec5edbe Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 22:24:06 +0200 Subject: [PATCH 125/191] plural to singular --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 4816be31e8ba5d..3911d415cf594b 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -38,5 +38,5 @@ jobs: sed '/ [0-9]* PRs$/{ s=^=
\n\n\n= s=$=\n\n= - }; s=^PR ==' | sed -z 's=\n---\nReports\n\n=\n
\n&=')" + }; s=^PR ==; s= 1 PRs= 1 PR=' | sed -z 's=\n---\nReports\n\n=\n\n&=')" ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" From 96d44cb661d1c26f801812f79f07424214a75c5b Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 1 Aug 2024 22:25:30 +0200 Subject: [PATCH 126/191] spaces --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 3911d415cf594b..077f583a207e25 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -38,5 +38,5 @@ jobs: sed '/ [0-9]* PRs$/{ s=^=
\n\n\n= s=$=\n\n= - }; s=^PR ==; s= 1 PRs= 1 PR=' | sed -z 's=\n---\nReports\n\n=\n
\n&=')" + }; s=^PR \(#[0-9]*\) =\1\n =; s= 1 PRs= 1 PR=' | sed -z 's=\n---\nReports\n\n=\n\n&=')" ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" From 00bfe68441baf04c41f244363471d9285e4835f2 Mon Sep 17 00:00:00 2001 From: damiano Date: Thu, 1 Aug 2024 22:56:17 +0200 Subject: [PATCH 127/191] Update .github/workflows/monthly_pr_report.yaml --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 077f583a207e25..6d736dbe263519 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -38,5 +38,5 @@ jobs: sed '/ [0-9]* PRs$/{ s=^=
\n\n\n= s=$=\n\n= - }; s=^PR \(#[0-9]*\) =\1\n =; s= 1 PRs= 1 PR=' | sed -z 's=\n---\nReports\n\n=\n
\n&=')" + }; s=^PR \(#[0-9]*\) =* \1\n =; s= 1 PRs= 1 PR=' | sed -z 's=\n---\nReports\n\n=\n\n&=')" ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" From 12f5456e910dbcdb247d22f26260332fe4905b46 Mon Sep 17 00:00:00 2001 From: damiano Date: Thu, 1 Aug 2024 23:01:34 +0200 Subject: [PATCH 128/191] Update .github/workflows/monthly_pr_report.yaml --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 6d736dbe263519..baef90b7aad454 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -38,5 +38,5 @@ jobs: sed '/ [0-9]* PRs$/{ s=^=
\n\n\n= s=$=\n\n= - }; s=^PR \(#[0-9]*\) =* \1\n =; s= 1 PRs= 1 PR=' | sed -z 's=\n---\nReports\n\n=\n
\n&=')" + }; s=^PR \(#[0-9]*\) =* \1 =; s= 1 PRs= 1 PR=' | sed -z 's=\n---\nReports\n\n=\n\n&=')" ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" From 44864ff38465e0db5f2d1cb177f9250a576eaede Mon Sep 17 00:00:00 2001 From: damiano Date: Thu, 1 Aug 2024 23:05:22 +0200 Subject: [PATCH 129/191] Remove PR title --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index baef90b7aad454..ec0845649f170e 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -38,5 +38,5 @@ jobs: sed '/ [0-9]* PRs$/{ s=^=
\n\n\n= s=$=\n\n= - }; s=^PR \(#[0-9]*\) =* \1 =; s= 1 PRs= 1 PR=' | sed -z 's=\n---\nReports\n\n=\n
\n&=')" + }; s=^PR \(#[0-9]* [^:]*\): .*=* \1 =; s= 1 PRs= 1 PR=' | sed -z 's=\n---\nReports\n\n=\n\n&=')" ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" From 2561ea3ec768e8910017bfac5e556274dba21725 Mon Sep 17 00:00:00 2001 From: damiano Date: Fri, 2 Aug 2024 04:54:07 +0200 Subject: [PATCH 130/191] remove unneeded line breaks --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index ec0845649f170e..abdb94acc00f1e 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -36,7 +36,7 @@ jobs: echo "${message}" message="$(echo "${message}" | sed '/ [0-9]* PRs$/{ - s=^=
\n\n\n= + s=^=
\n= s=$=\n\n= }; s=^PR \(#[0-9]* [^:]*\): .*=* \1 =; s= 1 PRs= 1 PR=' | sed -z 's=\n---\nReports\n\n=\n
\n&=')" ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" From 96d685b1b04d7caa6b0afc2d2870399449667c13 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 05:15:10 +0200 Subject: [PATCH 131/191] plural in all reports, format, remove initial --- .github/workflows/monthly_pr_report.yaml | 14 ++++++++++---- scripts/find_labels.sh | 2 +- 2 files changed, 11 insertions(+), 5 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index abdb94acc00f1e..bca06aa40d7062 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -35,8 +35,14 @@ jobs: message="$(printf '%s\n\n%s\n' "${title}" "$(./scripts/find_labels.sh "${{ github.repository }}")")" echo "${message}" message="$(echo "${message}" | - sed '/ [0-9]* PRs$/{ - s=^=
\n= - s=$=\n\n= - }; s=^PR \(#[0-9]* [^:]*\): .*=* \1 =; s= 1 PRs= 1 PR=' | sed -z 's=\n---\nReports\n\n=\n
\n&=')" + sed ' + / [0-9]* PRs$/{ + s=^=
\n= + s=$=\n\n= + } + s=^PR \(#[0-9]* [^:]*\): .*=* \1 =' | + sed -z ' + s=
=
= + s=\n---\nReports\n\n=\n
\n&= + ')" ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 31d29c88e0ac1c..0fe2c831e11778 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -72,7 +72,7 @@ findInRange "${1}" "${yr_mth}-16T00:00:00" "${end_date}" | sed -z 's=^\[==' gsub(/\[\]/, "Miscellaneous", tag) gsub(/["\][]/, "", tag) gsub(/,/, " ", tag) - printf("\n%s, %s PRs%s\n", tag, seen[order[i]], acc[order[i]]) + printf("\n%s, %s PR%s%s\n", tag, seen[order[i]], seen[order[i]] == "1" ? "" : "s", acc[order[i]]) } } ' From c66244f20771e5784c375311c6d179809eed14c7 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 05:20:27 +0200 Subject: [PATCH 132/191] shorten name --- scripts/find_labels.sh | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 0fe2c831e11778..afc861794c13ca 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -72,7 +72,8 @@ findInRange "${1}" "${yr_mth}-16T00:00:00" "${end_date}" | sed -z 's=^\[==' gsub(/\[\]/, "Miscellaneous", tag) gsub(/["\][]/, "", tag) gsub(/,/, " ", tag) - printf("\n%s, %s PR%s%s\n", tag, seen[order[i]], seen[order[i]] == "1" ? "" : "s", acc[order[i]]) + noPR=seen[order[i]] + printf("\n%s, %s PR%s%s\n", tag, noPR, noPR == "1" ? "" : "s", acc[order[i]]) } } ' From 79be0eb847df44b0c6f1c83284acc8bfbf8592c2 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 05:43:39 +0200 Subject: [PATCH 133/191] reports collapse --- .github/workflows/monthly_pr_report.yaml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index bca06aa40d7062..32ca4a63a02f24 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -43,6 +43,7 @@ jobs: s=^PR \(#[0-9]* [^:]*\): .*=* \1 =' | sed -z ' s=
=
= - s=\n---\nReports\n\n=\n
\n&= + s=\n---\nReports\n\n=\n
\n\n---\n
Reports\n\n= + s=\n---[\n]*=
&= ')" ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" From 6fdfb6ea2e2e048217ce00ecb71cddb1b407a8d3 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 05:45:57 +0200 Subject: [PATCH 134/191] details at end --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 32ca4a63a02f24..aeef9be1e38b5e 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -44,6 +44,6 @@ jobs: sed -z ' s=
=
= s=\n---\nReports\n\n=\n
\n\n---\n
Reports\n\n= - s=\n---[\n]*=
&= + s=\n---[\n]*$=
&= ')" ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" From d8ef988984e261a5645768b5742ef7263a7b54d1 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 05:47:59 +0200 Subject: [PATCH 135/191] close details --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index aeef9be1e38b5e..c240a7209918d7 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -44,6 +44,6 @@ jobs: sed -z ' s=
=
= s=\n---\nReports\n\n=\n
\n\n---\n
Reports\n\n= - s=\n---[\n]*$=
&= + s=\n---[\n]*$=
&= ')" ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" From a12987aafcc26ea07c5af3354b270f1eca92c1c7 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 05:49:11 +0200 Subject: [PATCH 136/191] space out final details --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index c240a7209918d7..8327f9c58f0920 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -44,6 +44,6 @@ jobs: sed -z ' s=
=
= s=\n---\nReports\n\n=\n
\n\n---\n
Reports\n\n= - s=\n---[\n]*$=
&= + s=\n---[\n]*$=\n\n
\n&= ')" ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" From ed02c7c4b82897691fbc5085483086c55c63e85b Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 05:51:17 +0200 Subject: [PATCH 137/191] one more line break --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 8327f9c58f0920..65247365c99a2e 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -43,7 +43,7 @@ jobs: s=^PR \(#[0-9]* [^:]*\): .*=* \1 =' | sed -z ' s=
=
= - s=\n---\nReports\n\n=\n
\n\n---\n
Reports\n\n= + s=\n---\nReports\n\n=\n
\n\n---\n\n
Reports\n\n= s=\n---[\n]*$=\n\n
\n&= ')" ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" From a62b5b468dd0941099521c2debf40720b3d1d968 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 06:00:24 +0200 Subject: [PATCH 138/191] extract date --- .github/workflows/monthly_pr_report.yaml | 2 +- scripts/find_labels.sh | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 65247365c99a2e..7108521b90d01d 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -32,7 +32,7 @@ jobs: printf $'Repository: %s\nBranch: %s\n' "${{ github.repository }}" "${BRANCH_NAME}" git checkout origin/adomani/yd_find_label scripts/find_labels.sh - message="$(printf '%s\n\n%s\n' "${title}" "$(./scripts/find_labels.sh "${{ github.repository }}")")" + message="$(printf '%s\n\n%s\n' "${title}" "$(./scripts/find_labels.sh "${{ github.repository }}" 2024-07)")" echo "${message}" message="$(echo "${message}" | sed ' diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index afc861794c13ca..92cb69a5f37b8b 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -1,8 +1,8 @@ #!/bin/bash # Check if required arguments are provided -if [ "$#" -ne 1 ]; then - printf $'Usage: %s \n\nFor instance `%s leanprover-community/mathlib4`\n\n' "${0}" "${0}" +if [ "$#" -ne 2 ]; then + printf $'Usage: %s \n\nFor instance `%s leanprover-community/mathlib4`\n\n' "${0}" "${0}" exit 1 fi @@ -36,8 +36,8 @@ echo "$prs" } # the current year and month -yr_mth=2024-07 #"$(date +%Y-%m)" -yr_mth_day=2024-07-01 +yr_mth="${2}" #"$(date +%Y-%m)" +yr_mth_day=${yr_mth}-01 start_date="${yr_mth_day}T00:00:00" end_date="$(date -d "${yr_mth_day} + 1 month - 1 day" +%Y-%m-%d)T23:59:59" From 903b0b52f7dec56b76de31e3de2b353481f497ca Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 06:02:09 +0200 Subject: [PATCH 139/191] in mathlib --- .github/workflows/monthly_pr_report.yaml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 7108521b90d01d..39e6cdd594152b 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -27,12 +27,14 @@ jobs: - name: blog report continue-on-error: true run: | + yrMth=2024-07 + mth="$(date -d "${yrMth}-01" '+%B')" PR="${{ github.event.pull_request.number }}" - title="### Month in Mathlib summary" + title="### ${mth} in Mathlib summary" printf $'Repository: %s\nBranch: %s\n' "${{ github.repository }}" "${BRANCH_NAME}" git checkout origin/adomani/yd_find_label scripts/find_labels.sh - message="$(printf '%s\n\n%s\n' "${title}" "$(./scripts/find_labels.sh "${{ github.repository }}" 2024-07)")" + message="$(printf '%s\n\n%s\n' "${title}" "$(./scripts/find_labels.sh "${{ github.repository }}" "${2024-07}")")" echo "${message}" message="$(echo "${message}" | sed ' From dd7594224daf1e7b4b25317d26b687777eaf71fa Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 06:06:11 +0200 Subject: [PATCH 140/191] show date --- scripts/find_labels.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 92cb69a5f37b8b..6dfb7fce057a94 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -5,7 +5,7 @@ if [ "$#" -ne 2 ]; then printf $'Usage: %s \n\nFor instance `%s leanprover-community/mathlib4`\n\n' "${0}" "${0}" exit 1 fi - +echo "Date: ${2}" rm -rf found_by_gh.txt found_by_git.txt findInRange () { From f6e8a4c9e114cfd7ace576d0f048199940160231 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 06:06:39 +0200 Subject: [PATCH 141/191] Do not continue on error --- .github/workflows/monthly_pr_report.yaml | 1 - 1 file changed, 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 39e6cdd594152b..7431adca841a13 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -25,7 +25,6 @@ jobs: ref: master - name: blog report - continue-on-error: true run: | yrMth=2024-07 mth="$(date -d "${yrMth}-01" '+%B')" From fcd366e4521d3eea4119a5058b34880114245bad Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 06:07:49 +0200 Subject: [PATCH 142/191] pass the date --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 7431adca841a13..816ca16ac3417d 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -33,7 +33,7 @@ jobs: printf $'Repository: %s\nBranch: %s\n' "${{ github.repository }}" "${BRANCH_NAME}" git checkout origin/adomani/yd_find_label scripts/find_labels.sh - message="$(printf '%s\n\n%s\n' "${title}" "$(./scripts/find_labels.sh "${{ github.repository }}" "${2024-07}")")" + message="$(printf '%s\n\n%s\n' "${title}" "$(./scripts/find_labels.sh "${{ github.repository }}" "${yrMth}")")" echo "${message}" message="$(echo "${message}" | sed ' From 6999c0787b920f7a071ebc6db085e8a54f1b1b65 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 06:08:45 +0200 Subject: [PATCH 143/191] do not print the date --- scripts/find_labels.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 6dfb7fce057a94..92cb69a5f37b8b 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -5,7 +5,7 @@ if [ "$#" -ne 2 ]; then printf $'Usage: %s \n\nFor instance `%s leanprover-community/mathlib4`\n\n' "${0}" "${0}" exit 1 fi -echo "Date: ${2}" + rm -rf found_by_gh.txt found_by_git.txt findInRange () { From f2e8804db78f61cec238859e1c8c04c25710fa85 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 06:31:57 +0200 Subject: [PATCH 144/191] start with comment --- .github/workflows/monthly_pr_report.yaml | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 816ca16ac3417d..2d55f507f2fe15 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -1,12 +1,18 @@ on: - pull_request + #pull_request + issue_comment: + types: [created, edited] + pull_request_review_comment: + types: [created, edited] name: Blog report jobs: + Monthly_PRs: - if: github.repository == 'leanprover-community/mathlib4' && github.event.pull_request.draft == false + if: contains(github.event.comment.body, 'mimblog') || ((github.event.issue.pull_request != 'null') && (startsWith(github.event.comment.body, 'mimblog') || contains(toJSON(github.event.comment.body), '\r\nmimblog'))) + #if: github.repository == 'leanprover-community/mathlib4' && github.event.pull_request.draft == false name: Blog draft runs-on: ubuntu-latest @@ -26,6 +32,7 @@ jobs: - name: blog report run: | + echo ${{ github.event.comment.body }} yrMth=2024-07 mth="$(date -d "${yrMth}-01" '+%B')" PR="${{ github.event.pull_request.number }}" From ac291cea56ce150cf84fda217c8124fbc9b9bd8a Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 06:33:30 +0200 Subject: [PATCH 145/191] environment variable --- .github/workflows/monthly_pr_report.yaml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 2d55f507f2fe15..cae5751698a3a0 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -19,6 +19,7 @@ jobs: env: GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} BRANCH_NAME: ${{ github.head_ref }} + COMMENT: ${{ github.event.comment.body }} steps: - name: cleanup @@ -32,7 +33,7 @@ jobs: - name: blog report run: | - echo ${{ github.event.comment.body }} + echo ${COMMENT} yrMth=2024-07 mth="$(date -d "${yrMth}-01" '+%B')" PR="${{ github.event.pull_request.number }}" From f6847e509bec169161fcbb973931313ba4549c1b Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 06:34:30 +0200 Subject: [PATCH 146/191] quotes --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index cae5751698a3a0..f691ffa77a733c 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -33,7 +33,7 @@ jobs: - name: blog report run: | - echo ${COMMENT} + echo "${COMMENT}" yrMth=2024-07 mth="$(date -d "${yrMth}-01" '+%B')" PR="${{ github.event.pull_request.number }}" From 26bea5d41dc58c251b7c02ed59fa0a6e496cacdc Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 06:37:37 +0200 Subject: [PATCH 147/191] print more --- .github/workflows/monthly_pr_report.yaml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index f691ffa77a733c..53d53e68e45c61 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -11,8 +11,8 @@ jobs: Monthly_PRs: - if: contains(github.event.comment.body, 'mimblog') || ((github.event.issue.pull_request != 'null') && (startsWith(github.event.comment.body, 'mimblog') || contains(toJSON(github.event.comment.body), '\r\nmimblog'))) - #if: github.repository == 'leanprover-community/mathlib4' && github.event.pull_request.draft == false + if: contains(github.event.comment.body, 'mimblog') || #|| ((github.event.issue.pull_request != 'null') && (startsWith(github.event.comment.body, 'mimblog') || contains(toJSON(github.event.comment.body), '\r\nmimblog'))) + github.repository == 'leanprover-community/mathlib4' && github.event.pull_request.draft == false name: Blog draft runs-on: ubuntu-latest From 353bec4e41816c841ae80050a5d8ae45253a6c44 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 06:38:53 +0200 Subject: [PATCH 148/191] one line --- .github/workflows/monthly_pr_report.yaml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 53d53e68e45c61..df10bfe2eac325 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -11,8 +11,7 @@ jobs: Monthly_PRs: - if: contains(github.event.comment.body, 'mimblog') || #|| ((github.event.issue.pull_request != 'null') && (startsWith(github.event.comment.body, 'mimblog') || contains(toJSON(github.event.comment.body), '\r\nmimblog'))) - github.repository == 'leanprover-community/mathlib4' && github.event.pull_request.draft == false + if: contains(github.event.comment.body, 'mimblog') || github.repository == 'leanprover-community/mathlib4' && github.event.pull_request.draft == false #|| ((github.event.issue.pull_request != 'null') && (startsWith(github.event.comment.body, 'mimblog') || contains(toJSON(github.event.comment.body), '\r\nmimblog'))) name: Blog draft runs-on: ubuntu-latest From eeb131839b8cba82d652af043e6adca0f0e7a651 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 06:40:38 +0200 Subject: [PATCH 149/191] another one line --- .github/workflows/monthly_pr_report.yaml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index df10bfe2eac325..0cc43463f86c37 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -1,12 +1,11 @@ +name: Blog report + on: - #pull_request - issue_comment: + issue_comment: #pull_request types: [created, edited] pull_request_review_comment: types: [created, edited] -name: Blog report - jobs: From a7d5a0f0bac2f8d4b224dd75eb4ac40021e7c842 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 06:42:11 +0200 Subject: [PATCH 150/191] add permissions --- .github/workflows/monthly_pr_report.yaml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 0cc43463f86c37..3e418ad7658863 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -13,6 +13,8 @@ jobs: if: contains(github.event.comment.body, 'mimblog') || github.repository == 'leanprover-community/mathlib4' && github.event.pull_request.draft == false #|| ((github.event.issue.pull_request != 'null') && (startsWith(github.event.comment.body, 'mimblog') || contains(toJSON(github.event.comment.body), '\r\nmimblog'))) name: Blog draft runs-on: ubuntu-latest + permissions: + pull-requests: write env: GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} From a8825b5876aa847df8d4e564f39fd6c8f7807973 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 06:43:22 +0200 Subject: [PATCH 151/191] also pull request --- .github/workflows/monthly_pr_report.yaml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 3e418ad7658863..720a3f53550456 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -1,7 +1,8 @@ name: Blog report on: - issue_comment: #pull_request + pull_request + issue_comment: types: [created, edited] pull_request_review_comment: types: [created, edited] From e9a69c57f90b15f4a02b9abc396775a7c97072b2 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 06:44:33 +0200 Subject: [PATCH 152/191] colon --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 720a3f53550456..2fff2cdb90dcf7 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -1,7 +1,7 @@ name: Blog report on: - pull_request + pull_request: issue_comment: types: [created, edited] pull_request_review_comment: From ca6cf861d58ec5a4916e04cbe6a1a598e1e4af41 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 06:48:31 +0200 Subject: [PATCH 153/191] comment better --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 2fff2cdb90dcf7..e3f87c6d13b3e5 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -34,7 +34,7 @@ jobs: - name: blog report run: | - echo "${COMMENT}" + echo "Comment: '${COMMENT}'" yrMth=2024-07 mth="$(date -d "${yrMth}-01" '+%B')" PR="${{ github.event.pull_request.number }}" From a6eca90ba342297982a41bb9c4b1dcab251457bb Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 06:49:43 +0200 Subject: [PATCH 154/191] hide pull request --- .github/workflows/monthly_pr_report.yaml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index e3f87c6d13b3e5..44b139230ea3d1 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -1,8 +1,7 @@ name: Blog report on: - pull_request: - issue_comment: + issue_comment: #pull_request: types: [created, edited] pull_request_review_comment: types: [created, edited] From 09db8a7bb186fcf2f5b471f5ee034b3452b9049c Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 06:52:04 +0200 Subject: [PATCH 155/191] only if --- .github/workflows/monthly_pr_report.yaml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 44b139230ea3d1..e12bc52f6e272c 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -7,10 +7,8 @@ on: types: [created, edited] jobs: - - Monthly_PRs: - if: contains(github.event.comment.body, 'mimblog') || github.repository == 'leanprover-community/mathlib4' && github.event.pull_request.draft == false #|| ((github.event.issue.pull_request != 'null') && (startsWith(github.event.comment.body, 'mimblog') || contains(toJSON(github.event.comment.body), '\r\nmimblog'))) + if: contains(github.event.comment.body, 'mimblog') #|| github.repository == 'leanprover-community/mathlib4' && github.event.pull_request.draft == false #|| ((github.event.issue.pull_request != 'null') && (startsWith(github.event.comment.body, 'mimblog') || contains(toJSON(github.event.comment.body), '\r\nmimblog'))) name: Blog draft runs-on: ubuntu-latest permissions: From b35c31e54c741ba95f130d9aebe3d5e0691acba5 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 06:52:41 +0200 Subject: [PATCH 156/191] no name --- .github/workflows/monthly_pr_report.yaml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index e12bc52f6e272c..455f68d5142f12 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -8,8 +8,7 @@ on: jobs: Monthly_PRs: - if: contains(github.event.comment.body, 'mimblog') #|| github.repository == 'leanprover-community/mathlib4' && github.event.pull_request.draft == false #|| ((github.event.issue.pull_request != 'null') && (startsWith(github.event.comment.body, 'mimblog') || contains(toJSON(github.event.comment.body), '\r\nmimblog'))) - name: Blog draft + if: contains(github.event.comment.body, 'mimblog') #|| github.repository == 'leanprover-community/mathlib4' && github.event.pull_request.draft == false #|| ((github.event.issue.pull_request != 'null') && (startsWith(github.event.comment.body, 'mimblog') || contains(toJSON(github.event.comment.body), '\r\nmimblog'))) #name: Blog draft runs-on: ubuntu-latest permissions: pull-requests: write From 4176673ed90008c420bd188bae618abdcfaa61bc Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 06:55:40 +0200 Subject: [PATCH 157/191] remove permissions --- .github/workflows/monthly_pr_report.yaml | 2 -- 1 file changed, 2 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 455f68d5142f12..9991bc32c59c0e 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -10,8 +10,6 @@ jobs: Monthly_PRs: if: contains(github.event.comment.body, 'mimblog') #|| github.repository == 'leanprover-community/mathlib4' && github.event.pull_request.draft == false #|| ((github.event.issue.pull_request != 'null') && (startsWith(github.event.comment.body, 'mimblog') || contains(toJSON(github.event.comment.body), '\r\nmimblog'))) #name: Blog draft runs-on: ubuntu-latest - permissions: - pull-requests: write env: GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} From 47b6d65cf7cde6ca6778573aee1c77b2743fee2b Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 06:57:34 +0200 Subject: [PATCH 158/191] run on any comment --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 9991bc32c59c0e..a79f69449deece 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -8,7 +8,7 @@ on: jobs: Monthly_PRs: - if: contains(github.event.comment.body, 'mimblog') #|| github.repository == 'leanprover-community/mathlib4' && github.event.pull_request.draft == false #|| ((github.event.issue.pull_request != 'null') && (startsWith(github.event.comment.body, 'mimblog') || contains(toJSON(github.event.comment.body), '\r\nmimblog'))) #name: Blog draft + #if: contains(github.event.comment.body, 'mimblog') #|| github.repository == 'leanprover-community/mathlib4' && github.event.pull_request.draft == false #|| ((github.event.issue.pull_request != 'null') && (startsWith(github.event.comment.body, 'mimblog') || contains(toJSON(github.event.comment.body), '\r\nmimblog'))) #name: Blog draft runs-on: ubuntu-latest env: From 90dc246e23c694c5eb8b183ba62877b6dba2d926 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 07:01:20 +0200 Subject: [PATCH 159/191] also deleted comments --- .github/workflows/monthly_pr_report.yaml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index a79f69449deece..3aa2da534830ee 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -2,9 +2,9 @@ name: Blog report on: issue_comment: #pull_request: - types: [created, edited] + types: [created, edited, deleted] pull_request_review_comment: - types: [created, edited] + types: [created, edited, deleted] jobs: Monthly_PRs: From a761751139ea46733d70491109c6264f8cddfa0e Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 07:22:27 +0200 Subject: [PATCH 160/191] cleanup comment --- .github/workflows/monthly_pr_report.yaml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 3aa2da534830ee..389b4d1c82c29f 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -2,13 +2,13 @@ name: Blog report on: issue_comment: #pull_request: - types: [created, edited, deleted] + types: [created, edited] pull_request_review_comment: - types: [created, edited, deleted] + types: [created, edited] jobs: Monthly_PRs: - #if: contains(github.event.comment.body, 'mimblog') #|| github.repository == 'leanprover-community/mathlib4' && github.event.pull_request.draft == false #|| ((github.event.issue.pull_request != 'null') && (startsWith(github.event.comment.body, 'mimblog') || contains(toJSON(github.event.comment.body), '\r\nmimblog'))) #name: Blog draft + if: contains(github.event.comment.body, 'mimblog') runs-on: ubuntu-latest env: @@ -28,11 +28,11 @@ jobs: - name: blog report run: | - echo "Comment: '${COMMENT}'" - yrMth=2024-07 + yrMth=${COMMENT/#* } + echo "yrMth: ${yrMth}" mth="$(date -d "${yrMth}-01" '+%B')" PR="${{ github.event.pull_request.number }}" - title="### ${mth} in Mathlib summary" + title="### ${mth} in Mathlib -- summary" printf $'Repository: %s\nBranch: %s\n' "${{ github.repository }}" "${BRANCH_NAME}" git checkout origin/adomani/yd_find_label scripts/find_labels.sh From 31112d70cf0a4524c78249d2d3249742d036f19b Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 07:25:35 +0200 Subject: [PATCH 161/191] two workflows: PR and comment --- .github/workflows/monthly_pr_comment.yaml | 53 +++++++++++++++++++++++ .github/workflows/monthly_pr_report.yaml | 19 ++++---- 2 files changed, 61 insertions(+), 11 deletions(-) create mode 100644 .github/workflows/monthly_pr_comment.yaml diff --git a/.github/workflows/monthly_pr_comment.yaml b/.github/workflows/monthly_pr_comment.yaml new file mode 100644 index 00000000000000..389b4d1c82c29f --- /dev/null +++ b/.github/workflows/monthly_pr_comment.yaml @@ -0,0 +1,53 @@ +name: Blog report + +on: + issue_comment: #pull_request: + types: [created, edited] + pull_request_review_comment: + types: [created, edited] + +jobs: + Monthly_PRs: + if: contains(github.event.comment.body, 'mimblog') + runs-on: ubuntu-latest + + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + BRANCH_NAME: ${{ github.head_ref }} + COMMENT: ${{ github.event.comment.body }} + + steps: + - name: cleanup + run: | + find . -name . -o -prune -exec rm -rf -- {} + + + - uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: master + + - name: blog report + run: | + yrMth=${COMMENT/#* } + echo "yrMth: ${yrMth}" + mth="$(date -d "${yrMth}-01" '+%B')" + PR="${{ github.event.pull_request.number }}" + title="### ${mth} in Mathlib -- summary" + + printf $'Repository: %s\nBranch: %s\n' "${{ github.repository }}" "${BRANCH_NAME}" + git checkout origin/adomani/yd_find_label scripts/find_labels.sh + message="$(printf '%s\n\n%s\n' "${title}" "$(./scripts/find_labels.sh "${{ github.repository }}" "${yrMth}")")" + echo "${message}" + message="$(echo "${message}" | + sed ' + / [0-9]* PRs$/{ + s=^=
\n= + s=$=\n\n= + } + s=^PR \(#[0-9]* [^:]*\): .*=* \1 =' | + sed -z ' + s=
=
= + s=\n---\nReports\n\n=\n
\n\n---\n\n
Reports\n\n= + s=\n---[\n]*$=\n\n
\n&= + ')" + ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 389b4d1c82c29f..816ca16ac3417d 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -1,20 +1,18 @@ -name: Blog report - on: - issue_comment: #pull_request: - types: [created, edited] - pull_request_review_comment: - types: [created, edited] + pull_request + +name: Blog report jobs: + Monthly_PRs: - if: contains(github.event.comment.body, 'mimblog') + if: github.repository == 'leanprover-community/mathlib4' && github.event.pull_request.draft == false + name: Blog draft runs-on: ubuntu-latest env: GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} BRANCH_NAME: ${{ github.head_ref }} - COMMENT: ${{ github.event.comment.body }} steps: - name: cleanup @@ -28,11 +26,10 @@ jobs: - name: blog report run: | - yrMth=${COMMENT/#* } - echo "yrMth: ${yrMth}" + yrMth=2024-07 mth="$(date -d "${yrMth}-01" '+%B')" PR="${{ github.event.pull_request.number }}" - title="### ${mth} in Mathlib -- summary" + title="### ${mth} in Mathlib summary" printf $'Repository: %s\nBranch: %s\n' "${{ github.repository }}" "${BRANCH_NAME}" git checkout origin/adomani/yd_find_label scripts/find_labels.sh From c7967a90d74406b64e117d4339f14804c4511ce8 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 07:29:04 +0200 Subject: [PATCH 162/191] add explicit repository --- .github/workflows/monthly_pr_comment.yaml | 1 + .github/workflows/monthly_pr_report.yaml | 1 + 2 files changed, 2 insertions(+) diff --git a/.github/workflows/monthly_pr_comment.yaml b/.github/workflows/monthly_pr_comment.yaml index 389b4d1c82c29f..b253899459164b 100644 --- a/.github/workflows/monthly_pr_comment.yaml +++ b/.github/workflows/monthly_pr_comment.yaml @@ -23,6 +23,7 @@ jobs: - uses: actions/checkout@v4 with: + repository: mathlib4 fetch-depth: 0 ref: master diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 816ca16ac3417d..6d403ff5adf4cf 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -21,6 +21,7 @@ jobs: - uses: actions/checkout@v4 with: + repository: mathlib4 fetch-depth: 0 ref: master From 426154018628f5edba8e504ea034c057ce91f963 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 07:34:31 +0200 Subject: [PATCH 163/191] remove comment action --- .github/workflows/monthly_pr_comment.yaml | 54 ----------------------- 1 file changed, 54 deletions(-) delete mode 100644 .github/workflows/monthly_pr_comment.yaml diff --git a/.github/workflows/monthly_pr_comment.yaml b/.github/workflows/monthly_pr_comment.yaml deleted file mode 100644 index b253899459164b..00000000000000 --- a/.github/workflows/monthly_pr_comment.yaml +++ /dev/null @@ -1,54 +0,0 @@ -name: Blog report - -on: - issue_comment: #pull_request: - types: [created, edited] - pull_request_review_comment: - types: [created, edited] - -jobs: - Monthly_PRs: - if: contains(github.event.comment.body, 'mimblog') - runs-on: ubuntu-latest - - env: - GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} - BRANCH_NAME: ${{ github.head_ref }} - COMMENT: ${{ github.event.comment.body }} - - steps: - - name: cleanup - run: | - find . -name . -o -prune -exec rm -rf -- {} + - - - uses: actions/checkout@v4 - with: - repository: mathlib4 - fetch-depth: 0 - ref: master - - - name: blog report - run: | - yrMth=${COMMENT/#* } - echo "yrMth: ${yrMth}" - mth="$(date -d "${yrMth}-01" '+%B')" - PR="${{ github.event.pull_request.number }}" - title="### ${mth} in Mathlib -- summary" - - printf $'Repository: %s\nBranch: %s\n' "${{ github.repository }}" "${BRANCH_NAME}" - git checkout origin/adomani/yd_find_label scripts/find_labels.sh - message="$(printf '%s\n\n%s\n' "${title}" "$(./scripts/find_labels.sh "${{ github.repository }}" "${yrMth}")")" - echo "${message}" - message="$(echo "${message}" | - sed ' - / [0-9]* PRs$/{ - s=^=
\n= - s=$=\n\n= - } - s=^PR \(#[0-9]* [^:]*\): .*=* \1 =' | - sed -z ' - s=
=
= - s=\n---\nReports\n\n=\n
\n\n---\n\n
Reports\n\n= - s=\n---[\n]*$=\n\n
\n&= - ')" - ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" From acaf9f3e182ed14548325917dd6e173e7365cf00 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 08:34:24 +0200 Subject: [PATCH 164/191] use leanprover --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 6d403ff5adf4cf..829420b9c61d89 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -21,7 +21,7 @@ jobs: - uses: actions/checkout@v4 with: - repository: mathlib4 + repository: leanprover-community/mathlib4 fetch-depth: 0 ref: master From 53d741bb540c643f0544b0b7de07e692c839525a Mon Sep 17 00:00:00 2001 From: damiano Date: Fri, 16 Jan 2026 16:14:37 +0100 Subject: [PATCH 165/191] Update .github/workflows/monthly_pr_report.yaml --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 829420b9c61d89..8d0a867f26a8ed 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -27,7 +27,7 @@ jobs: - name: blog report run: | - yrMth=2024-07 + yrMth="$(date +%Y-%m)" # format: 2024-07 mth="$(date -d "${yrMth}-01" '+%B')" PR="${{ github.event.pull_request.number }}" title="### ${mth} in Mathlib summary" From a3970dcd90a9288c42c4f53bcc57fe93a367d6b4 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Fri, 16 Jan 2026 16:24:34 +0100 Subject: [PATCH 166/191] log --- .github/workflows/monthly_pr_report.yaml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 8d0a867f26a8ed..f536eecade9bef 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -29,6 +29,7 @@ jobs: run: | yrMth="$(date +%Y-%m)" # format: 2024-07 mth="$(date -d "${yrMth}-01" '+%B')" + printf $'Date: %s, month: %s\n' "${yrMth}" "${mth}" PR="${{ github.event.pull_request.number }}" title="### ${mth} in Mathlib summary" From c8f204f231e404e1267d76388f3d03f73fff393b Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Fri, 16 Jan 2026 16:28:32 +0100 Subject: [PATCH 167/191] print also reformatted text --- .github/workflows/monthly_pr_report.yaml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index f536eecade9bef..49fb39f4d31a4e 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -49,4 +49,7 @@ jobs: s=\n---\nReports\n\n=\n
\n\n---\n\n
Reports\n\n= s=\n---[\n]*$=\n\n
\n&= ')" + echo "---" + echo "---" + echo "${message}" ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" From a6f91c4ef3d9be70a0bef4f9c575069a54585edd Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Fri, 16 Jan 2026 22:49:26 +0100 Subject: [PATCH 168/191] Add year --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 49fb39f4d31a4e..4565a2f2d9e00a 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -31,7 +31,7 @@ jobs: mth="$(date -d "${yrMth}-01" '+%B')" printf $'Date: %s, month: %s\n' "${yrMth}" "${mth}" PR="${{ github.event.pull_request.number }}" - title="### ${mth} in Mathlib summary" + title="### ${mth} $(date +%Y) in Mathlib summary" printf $'Repository: %s\nBranch: %s\n' "${{ github.repository }}" "${BRANCH_NAME}" git checkout origin/adomani/yd_find_label scripts/find_labels.sh From d403191f879952cb88f01c5a198da222610d7417 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Fri, 16 Jan 2026 22:52:43 +0100 Subject: [PATCH 169/191] use a file --- .github/workflows/monthly_pr_report.yaml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 4565a2f2d9e00a..b4e38b6f63d154 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -37,7 +37,7 @@ jobs: git checkout origin/adomani/yd_find_label scripts/find_labels.sh message="$(printf '%s\n\n%s\n' "${title}" "$(./scripts/find_labels.sh "${{ github.repository }}" "${yrMth}")")" echo "${message}" - message="$(echo "${message}" | + echo "${message}" | sed ' / [0-9]* PRs$/{ s=^=
\n= @@ -48,8 +48,7 @@ jobs: s=
=
= s=\n---\nReports\n\n=\n
\n\n---\n\n
Reports\n\n= s=\n---[\n]*$=\n\n
\n&= - ')" + ' | tee "${yrMth}_in_mathlib.md" echo "---" echo "---" - echo "${message}" - ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" + ./scripts/update_PR_comment.sh "${yrMth}_in_mathlib.md" "${title}" "${PR}" From 6280d6eb0609405a3b7c2c80bc7c08bde7dfcab8 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Fri, 16 Jan 2026 22:59:05 +0100 Subject: [PATCH 170/191] tmp_file --- .github/workflows/monthly_pr_report.yaml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index b4e38b6f63d154..2472087e630a7c 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -29,7 +29,8 @@ jobs: run: | yrMth="$(date +%Y-%m)" # format: 2024-07 mth="$(date -d "${yrMth}-01" '+%B')" - printf $'Date: %s, month: %s\n' "${yrMth}" "${mth}" + tmp_file="${yrMth}_in_mathlib.md" + printf $'Date: %s, month: %s\ntemp file: %s\n' "${yrMth}" "${mth}" "${tmp_file}" PR="${{ github.event.pull_request.number }}" title="### ${mth} $(date +%Y) in Mathlib summary" @@ -48,7 +49,7 @@ jobs: s=
=
= s=\n---\nReports\n\n=\n
\n\n---\n\n
Reports\n\n= s=\n---[\n]*$=\n\n
\n&= - ' | tee "${yrMth}_in_mathlib.md" + ' | tee "${tmp_file}" echo "---" echo "---" - ./scripts/update_PR_comment.sh "${yrMth}_in_mathlib.md" "${title}" "${PR}" + ./scripts/update_PR_comment.sh "${tmp_file}" "${title}" "${PR}" From e98868eca5b5e00c66fe34dae42a00d559287a18 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Fri, 16 Jan 2026 23:00:55 +0100 Subject: [PATCH 171/191] rename secret --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 2472087e630a7c..3a2d86ec253027 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -11,7 +11,7 @@ jobs: runs-on: ubuntu-latest env: - GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} BRANCH_NAME: ${{ github.head_ref }} steps: From b3601ad7ec0a53972f9149e093736dd8288cb7a9 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Fri, 16 Jan 2026 23:09:42 +0100 Subject: [PATCH 172/191] add readme entry --- scripts/README.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/scripts/README.md b/scripts/README.md index e0195975c4ed82..56f7cd1f6d64df 100644 --- a/scripts/README.md +++ b/scripts/README.md @@ -123,6 +123,10 @@ to learn about it as well! displaying human-readable output. - `verify_commits_summary.sh` generates a markdown PR comment from `verify_commits.sh` JSON output. Used by CI to post verification summaries on pull requests. +- `find_labels.sh` generates a monthly report of all PRs merged into `master` by Bors for a given + GitHub repository, grouping them by labels and comparing them with commits found in the local git + history. It also highlights discrepancies between PRs detected via the GitHub CLI and those + inferred from commit messages (mostly for debugging). **Managing nightly-testing and bump branches** - `create-adaptation-pr.sh` implements some of the steps in the workflow described at From d5ff60559f7b6d26d7c25b9108a0c9632ef8cd37 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Fri, 16 Jan 2026 23:12:53 +0100 Subject: [PATCH 173/191] more documentation --- scripts/find_labels.sh | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 92cb69a5f37b8b..06fc7f4ab4371e 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -1,4 +1,16 @@ #!/bin/bash + : << 'BASH_MODULE_DOCS' + +Usage: ./script.sh owner/repo YYYY-MM + +The script summarizes PRs by label and author in the given year-month range in the input GitHub repository. + +It assumes that +* the merged PRs have been `[Merged by Bors]`; +* `gh auth status` is set for the repo; +* `jq` is installed. + +BASH_MODULE_DOCS # Check if required arguments are provided if [ "$#" -ne 2 ]; then From b0f2ae861d71b16a7df37b2d662666fae949b6b4 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Fri, 16 Jan 2026 23:24:37 +0100 Subject: [PATCH 174/191] commented cron, process yesterday --- .github/workflows/monthly_pr_report.yaml | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 3a2d86ec253027..da30c828b47443 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -1,5 +1,8 @@ on: pull_request + #schedule: + #- cron: '0 0 1 * *' # Runs at 00:00 on day 1 of the month + #workflow_dispatch: name: Blog report @@ -27,12 +30,15 @@ jobs: - name: blog report run: | - yrMth="$(date +%Y-%m)" # format: 2024-07 + # The job runs on the first of each month and will process the date for the previous month + yr="$(date --date=yesterday +\%Y)" + mm="$(date --date=yesterday +\%m)" + yrMth="${yr}-${mm}" # format: 2024-07 mth="$(date -d "${yrMth}-01" '+%B')" tmp_file="${yrMth}_in_mathlib.md" printf $'Date: %s, month: %s\ntemp file: %s\n' "${yrMth}" "${mth}" "${tmp_file}" PR="${{ github.event.pull_request.number }}" - title="### ${mth} $(date +%Y) in Mathlib summary" + title="### ${mth} ${yr} in Mathlib summary" printf $'Repository: %s\nBranch: %s\n' "${{ github.repository }}" "${BRANCH_NAME}" git checkout origin/adomani/yd_find_label scripts/find_labels.sh From 1d3cbaab4a1d500233bbae6fcd13f5b2f82b51b4 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Fri, 16 Jan 2026 23:26:16 +0100 Subject: [PATCH 175/191] quotes --- .github/workflows/monthly_pr_report.yaml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index da30c828b47443..75ae5180acd9d7 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -31,8 +31,8 @@ jobs: - name: blog report run: | # The job runs on the first of each month and will process the date for the previous month - yr="$(date --date=yesterday +\%Y)" - mm="$(date --date=yesterday +\%m)" + yr="$(date --date=yesterday '+%Y')" + mm="$(date --date=yesterday '+%m')" yrMth="${yr}-${mm}" # format: 2024-07 mth="$(date -d "${yrMth}-01" '+%B')" tmp_file="${yrMth}_in_mathlib.md" From 46db28dfd35a708db916f4969b56e3ffad49ec27 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Sat, 17 Jan 2026 17:58:45 +0100 Subject: [PATCH 176/191] 2 weeks --- scripts/find_labels.sh | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 06fc7f4ab4371e..40d0d40b86fda9 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -52,11 +52,13 @@ yr_mth="${2}" #"$(date +%Y-%m)" yr_mth_day=${yr_mth}-01 start_date="${yr_mth_day}T00:00:00" -end_date="$(date -d "${yr_mth_day} + 1 month - 1 day" +%Y-%m-%d)T23:59:59" +#end_date="$(date -d "${yr_mth_day} + 1 month - 1 day" +%Y-%m-%d)T23:59:59" +end_date="$(date -d "${yr_mth_day} + 2 weeks" +%Y-%m-%d)T23:59:59" mth="$(date -d "${yr_mth_day}" '+%B')" prev_mth="$(date -d "${yr_mth_day} - 1 day" '+%B')" -next_mth="$(date -d "${yr_mth_day} + 1 month" '+%B')" +#next_mth="$(date -d "${yr_mth_day} + 1 month" '+%B')" +next_mth="$(date -d "${yr_mth_day} + 2 weeks" '+%B')" commits_in_range="$(git log --since="${start_date}" --until="${end_date}" --pretty=oneline | wc -l)" From 1a27cd0b9dc2e89caa1db0dc5b8cfa6f919c06f2 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Sun, 18 Jan 2026 10:36:54 +0100 Subject: [PATCH 177/191] script name in usage --- scripts/find_labels.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 40d0d40b86fda9..6a7583f1aeaac3 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -1,7 +1,7 @@ #!/bin/bash : << 'BASH_MODULE_DOCS' -Usage: ./script.sh owner/repo YYYY-MM +Usage: ./scripts/find_labels.sh owner/repo YYYY-MM The script summarizes PRs by label and author in the given year-month range in the input GitHub repository. @@ -28,7 +28,7 @@ repository="${1}" startDate="${2}" endDate="${3}" -# find how many commits to master there have been in the last month +# find how many commits to master there have been in the given range commits_in_range="$(git log --since="${startDate}" --until="${endDate}" --pretty=oneline | wc -l)" # Retrieve merged PRs from the given range From fabd9d1575bbb9396049079566b489806b32fdf6 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Sun, 18 Jan 2026 10:55:20 +0100 Subject: [PATCH 178/191] better usage suggestion --- scripts/find_labels.sh | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 6a7583f1aeaac3..879ce81a3d6dda 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -14,7 +14,8 @@ BASH_MODULE_DOCS # Check if required arguments are provided if [ "$#" -ne 2 ]; then - printf $'Usage: %s \n\nFor instance `%s leanprover-community/mathlib4`\n\n' "${0}" "${0}" + printf $'Usage: %s \n\n' "${0}" + printf $'For instance `%s leanprover-community/mathlib4 %s`\n\n' "${0}" "$(date +%Y-%m)" exit 1 fi From 462985f2818a30604a6c19735de0ca19ff8f059b Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Sun, 18 Jan 2026 11:08:09 +0100 Subject: [PATCH 179/191] better module docs and usage info --- scripts/find_labels.sh | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 879ce81a3d6dda..211612f5910198 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -1,7 +1,7 @@ #!/bin/bash : << 'BASH_MODULE_DOCS' -Usage: ./scripts/find_labels.sh owner/repo YYYY-MM +Usage: ./scripts/find_labels.sh owner/repo start_date end_date The script summarizes PRs by label and author in the given year-month range in the input GitHub repository. @@ -13,9 +13,10 @@ It assumes that BASH_MODULE_DOCS # Check if required arguments are provided -if [ "$#" -ne 2 ]; then - printf $'Usage: %s \n\n' "${0}" - printf $'For instance `%s leanprover-community/mathlib4 %s`\n\n' "${0}" "$(date +%Y-%m)" +if [ "$#" -ne 3 ]; then + printf $'Usage: %s \n\n' "${0}" + printf $'For instance `%s leanprover-community/mathlib4 %s %s`\n\n' "${0}" "$(date -d "today - 2 weeks" +%Y-%m-%d)" "$(date -d "today" +%Y-%m-%d)" + printf $'The dates can also include time signatures, as in %s\n' "$(date -d '+1 hour' '+%FT%T')" exit 1 fi From 9eaa9feaa44623b124314abf5a5041beabfbbdf0 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Sun, 18 Jan 2026 12:11:20 +0100 Subject: [PATCH 180/191] better start date and end dates --- scripts/find_labels.sh | 40 ++++++++++------------------------------ 1 file changed, 10 insertions(+), 30 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 211612f5910198..c2a1f497d4bb58 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -1,7 +1,7 @@ #!/bin/bash : << 'BASH_MODULE_DOCS' -Usage: ./scripts/find_labels.sh owner/repo start_date end_date +Usage: ./scripts/find_labels.sh owner/repo startDate endDate The script summarizes PRs by label and author in the given year-month range in the input GitHub repository. @@ -14,7 +14,7 @@ BASH_MODULE_DOCS # Check if required arguments are provided if [ "$#" -ne 3 ]; then - printf $'Usage: %s \n\n' "${0}" + printf $'Usage: %s \n\n' "${0}" printf $'For instance `%s leanprover-community/mathlib4 %s %s`\n\n' "${0}" "$(date -d "today - 2 weeks" +%Y-%m-%d)" "$(date -d "today" +%Y-%m-%d)" printf $'The dates can also include time signatures, as in %s\n' "$(date -d '+1 hour' '+%FT%T')" exit 1 @@ -22,8 +22,6 @@ fi rm -rf found_by_gh.txt found_by_git.txt -findInRange () { - repository="${1}" # Get the start and end dates @@ -46,34 +44,16 @@ echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "(# git log --pretty=oneline --since="${startDate}" --until="${endDate}" | sed -n 's=.*\((#[0-9]*)\)$=\1=p' | sort >> found_by_git.txt -echo "$prs" -} - -# the current year and month -yr_mth="${2}" #"$(date +%Y-%m)" -yr_mth_day=${yr_mth}-01 - -start_date="${yr_mth_day}T00:00:00" -#end_date="$(date -d "${yr_mth_day} + 1 month - 1 day" +%Y-%m-%d)T23:59:59" -end_date="$(date -d "${yr_mth_day} + 2 weeks" +%Y-%m-%d)T23:59:59" - -mth="$(date -d "${yr_mth_day}" '+%B')" -prev_mth="$(date -d "${yr_mth_day} - 1 day" '+%B')" -#next_mth="$(date -d "${yr_mth_day} + 1 month" '+%B')" -next_mth="$(date -d "${yr_mth_day} + 2 weeks" '+%B')" - -commits_in_range="$(git log --since="${start_date}" --until="${end_date}" --pretty=oneline | wc -l)" +commits_in_range="$(git log --since="${startDate}" --until="${endDate}" --pretty=oneline | wc -l)" -printf $'\n\nBetween %s and %s there were\n' "${yr_mth_day}" "${end_date/%T*}" +printf $'\n\nBetween %s and %s there were\n' "${startDate}" "${endDate/%T*}" printf $'* %s commits to `master` and\n' "${commits_in_range}" -( -findInRange "${1}" "${start_date}" "${yr_mth}-15T23:59:59" | sed -z 's=]\n*$=,\n=' -findInRange "${1}" "${yr_mth}-16T00:00:00" "${end_date}" | sed -z 's=^\[==' -) | jq -S -r '.[] | - select(.title | startswith("[Merged by Bors]")) | - "\(.labels | map(.name | select(startswith("t-"))) ) PR #\(.number) \(if .author.name == "" then .author.login else .author.name end): \(.title)"' | +echo "$prs" | + jq -S -r '.[] | + select(.title | startswith("[Merged by Bors]")) | + "\(.labels | map(.name | select(startswith("t-"))) ) PR #\(.number) \(if .author.name == "" then .author.login else .author.name end): \(.title)"' | sort | awk 'BEGIN{ labels=""; con=0; total=0 } { total++ @@ -103,14 +83,14 @@ if [ -z "${only_gh}" ] then printf $'* All PRs are accounted for!\n' else - printf $'* PRs not corresponding to a commit (merged in %s, closed in %s?)\n%s\n' "${prev_mth}" "${mth}" "${only_gh}" + printf $'* PRs not corresponding to a commit (merged before %s, closed on %s?)\n%s\n' "${startDate}" "${startDate}" "${only_gh}" fi if [ -z "${only_git}" ] then printf $'\n* All commits are accounted for!\n' else - printf $'\n* PRs not found by `gh` (merged in %s, closed in %s?)\n%s\n' "${mth}" "${next_mth}" "${only_git}" + printf $'\n* PRs not found by `gh` (merged by %s, closed after %s?)\n%s\n' "${endDate}" "${endDate}" "${only_git}" fi printf -- $'---\n' From ee58ce6138f2449a912e8ded0891b208105a60ea Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Sun, 18 Jan 2026 12:19:14 +0100 Subject: [PATCH 181/191] adjust end date --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 75ae5180acd9d7..2a98ae61cbc4cf 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -42,7 +42,7 @@ jobs: printf $'Repository: %s\nBranch: %s\n' "${{ github.repository }}" "${BRANCH_NAME}" git checkout origin/adomani/yd_find_label scripts/find_labels.sh - message="$(printf '%s\n\n%s\n' "${title}" "$(./scripts/find_labels.sh "${{ github.repository }}" "${yrMth}")")" + message="$(printf '%s\n\n%s\n' "${title}" "$(./scripts/find_labels.sh "${{ github.repository }}" "${yrMth}-01" "$(date -d "$(date +%Y%m01) +1 month -1 day" +%Y-%m-%d)")")" echo "${message}" echo "${message}" | sed ' From eda64e444fa92023f4fc7264380ce435500ae950 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Sun, 18 Jan 2026 12:55:25 +0100 Subject: [PATCH 182/191] formatting for zulip --- .github/workflows/monthly_pr_report.yaml | 30 +++++++++++++++++------- 1 file changed, 22 insertions(+), 8 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 2a98ae61cbc4cf..50d8d33a591f39 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -44,17 +44,31 @@ jobs: git checkout origin/adomani/yd_find_label scripts/find_labels.sh message="$(printf '%s\n\n%s\n' "${title}" "$(./scripts/find_labels.sh "${{ github.repository }}" "${yrMth}-01" "$(date -d "$(date +%Y%m01) +1 month -1 day" +%Y-%m-%d)")")" echo "${message}" + + # formatting for GitHub + #echo "${message}" | + # sed ' + # / [0-9]* PRs$/{ + # s=^=
\n= + # s=$=\n\n= + # } + # s=^PR \(#[0-9]* [^:]*\): .*=* \1 =' | + # sed -z ' + # s=
=
= + # s=\n---\nReports\n\n=\n
\n\n---\n\n
Reports\n\n= + # s=\n---[\n]*$=\n\n
\n&= + # ' | tee "${tmp_file}" + + # formatting for Zulip echo "${message}" | sed ' - / [0-9]* PRs$/{ - s=^=
\n= - s=$=\n\n= - } - s=^PR \(#[0-9]* [^:]*\): .*=* \1 =' | + / [0-9]* PR[s]*$/{ + s=^=```\n\n```spoiler = + #s=$=\n```\n= + }' | sed -z ' - s=
=
= - s=\n---\nReports\n\n=\n
\n\n---\n\n
Reports\n\n= - s=\n---[\n]*$=\n\n
\n&= + s=\n```\n=\n= + s=\n\n```\n=\n```\n=g ' | tee "${tmp_file}" echo "---" echo "---" From f1d4db7e814fbf9534bbd2f6374e042947414361 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Sun, 18 Jan 2026 13:05:38 +0100 Subject: [PATCH 183/191] close last spoiler --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 50d8d33a591f39..59439f52be9e1d 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -64,11 +64,11 @@ jobs: sed ' / [0-9]* PR[s]*$/{ s=^=```\n\n```spoiler = - #s=$=\n```\n= }' | sed -z ' s=\n```\n=\n= s=\n\n```\n=\n```\n=g + s=\n$=\n```\n= ' | tee "${tmp_file}" echo "---" echo "---" From 84a4e516635a162e4ee0cc16df4babed80b19069 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Sun, 18 Jan 2026 13:12:01 +0100 Subject: [PATCH 184/191] expose both formats --- .github/workflows/monthly_pr_report.yaml | 45 +++++++++++++----------- 1 file changed, 24 insertions(+), 21 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 59439f52be9e1d..f24e9b3bba7b44 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -45,31 +45,34 @@ jobs: message="$(printf '%s\n\n%s\n' "${title}" "$(./scripts/find_labels.sh "${{ github.repository }}" "${yrMth}-01" "$(date -d "$(date +%Y%m01) +1 month -1 day" +%Y-%m-%d)")")" echo "${message}" - # formatting for GitHub - #echo "${message}" | - # sed ' - # / [0-9]* PRs$/{ - # s=^=
\n= - # s=$=\n\n= - # } - # s=^PR \(#[0-9]* [^:]*\): .*=* \1 =' | - # sed -z ' - # s=
=
= - # s=\n---\nReports\n\n=\n
\n\n---\n\n
Reports\n\n= - # s=\n---[\n]*$=\n\n
\n&= - # ' | tee "${tmp_file}" + formatForGitHub () { + echo "${1}" | + sed ' + / [0-9]* PRs$/{ + s=^=
\n= + s=$=\n\n= + } + s=^PR \(#[0-9]* [^:]*\): .*=* \1 =' | + sed -z ' + s=
=
= + s=\n---\nReports\n\n=\n
\n\n---\n\n
Reports\n\n= + s=\n---[\n]*$=\n\n
\n&= + ' + } - # formatting for Zulip - echo "${message}" | + formatForZulip () { + echo "${1}" | sed ' - / [0-9]* PR[s]*$/{ - s=^=```\n\n```spoiler = + / [0-9]* PR[s]*$/{ + s=^=```\n\n```spoiler = }' | - sed -z ' + sed -z ' s=\n```\n=\n= s=\n\n```\n=\n```\n=g s=\n$=\n```\n= - ' | tee "${tmp_file}" - echo "---" - echo "---" + ' + } + + formatForZulip "${message}" | tee "${tmp_file}" + ./scripts/update_PR_comment.sh "${tmp_file}" "${title}" "${PR}" From ee7bbaa4573cf4c066cd40ead9986a90871b1292 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Sun, 18 Jan 2026 13:16:25 +0100 Subject: [PATCH 185/191] disable shellcheck --- .github/workflows/monthly_pr_report.yaml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index f24e9b3bba7b44..6821a2102b44aa 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -62,6 +62,7 @@ jobs: formatForZulip () { echo "${1}" | + # shellcheck disable=SC2016 # backticks should not be expanded, since they are Zulip markdown syntax sed ' / [0-9]* PR[s]*$/{ s=^=```\n\n```spoiler = From f690848aa8dad240e6dde9849707db287b82183a Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Sun, 18 Jan 2026 13:17:45 +0100 Subject: [PATCH 186/191] better shellcheck placement --- .github/workflows/monthly_pr_report.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 6821a2102b44aa..00affadafb8903 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -60,9 +60,9 @@ jobs: ' } + # shellcheck disable=SC2016 # backticks should not be expanded, since they are Zulip markdown syntax formatForZulip () { echo "${1}" | - # shellcheck disable=SC2016 # backticks should not be expanded, since they are Zulip markdown syntax sed ' / [0-9]* PR[s]*$/{ s=^=```\n\n```spoiler = From 351e11b60107ebd78cf283d71f137a184cff48d5 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Sun, 18 Jan 2026 13:29:44 +0100 Subject: [PATCH 187/191] move formatting to find_labels --- .github/workflows/monthly_pr_report.yaml | 32 +------------------- scripts/find_labels.sh | 38 +++++++++++++++++++++--- 2 files changed, 35 insertions(+), 35 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 00affadafb8903..640d16934c6847 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -43,37 +43,7 @@ jobs: printf $'Repository: %s\nBranch: %s\n' "${{ github.repository }}" "${BRANCH_NAME}" git checkout origin/adomani/yd_find_label scripts/find_labels.sh message="$(printf '%s\n\n%s\n' "${title}" "$(./scripts/find_labels.sh "${{ github.repository }}" "${yrMth}-01" "$(date -d "$(date +%Y%m01) +1 month -1 day" +%Y-%m-%d)")")" - echo "${message}" - formatForGitHub () { - echo "${1}" | - sed ' - / [0-9]* PRs$/{ - s=^=
\n= - s=$=\n\n= - } - s=^PR \(#[0-9]* [^:]*\): .*=* \1 =' | - sed -z ' - s=
=
= - s=\n---\nReports\n\n=\n
\n\n---\n\n
Reports\n\n= - s=\n---[\n]*$=\n\n
\n&= - ' - } - - # shellcheck disable=SC2016 # backticks should not be expanded, since they are Zulip markdown syntax - formatForZulip () { - echo "${1}" | - sed ' - / [0-9]* PR[s]*$/{ - s=^=```\n\n```spoiler = - }' | - sed -z ' - s=\n```\n=\n= - s=\n\n```\n=\n```\n=g - s=\n$=\n```\n= - ' - } - - formatForZulip "${message}" | tee "${tmp_file}" + echo "${message}" | tee "${tmp_file}" ./scripts/update_PR_comment.sh "${tmp_file}" "${title}" "${PR}" diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index c2a1f497d4bb58..bb16a2c7f32965 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -50,7 +50,7 @@ printf $'\n\nBetween %s and %s there were\n' "${startDate}" "${endDate/%T*}" printf $'* %s commits to `master` and\n' "${commits_in_range}" -echo "$prs" | +formattedPRs="$(echo "$prs" | jq -S -r '.[] | select(.title | startswith("[Merged by Bors]")) | "\(.labels | map(.name | select(startswith("t-"))) ) PR #\(.number) \(if .author.name == "" then .author.login else .author.name end): \(.title)"' | @@ -72,12 +72,42 @@ echo "$prs" | printf("\n%s, %s PR%s%s\n", tag, noPR, noPR == "1" ? "" : "s", acc[order[i]]) } } - ' + ')" + +formatForGitHub () { + echo "${1}" | + sed ' + / [0-9]* PRs$/{ + s=^=
\n= + s=$=\n\n= + } + s=^PR \(#[0-9]* [^:]*\): .*=* \1 =' | + sed -z ' + s=
=
= + s=\n---\nReports\n\n=\n
\n\n---\n\n
Reports\n\n= + s=\n---[\n]*$=\n\n
\n&= + ' +} + +formatForZulip () { + echo "${1}" | + sed ' + / [0-9]* PR[s]*$/{ + s=^=```\n\n```spoiler = + }' | + sed -z ' + s=\n```\n=\n= + s=\n\n```\n=\n```\n=g + s=\n$=\n```\n= + ' +} + +formatForZulip "${formattedPRs}" only_gh="$( comm -23 <(sort found_by_gh.txt) <(sort found_by_git.txt) | sed 's=^= =' | tr -d '()')" only_git="$(comm -13 <(sort found_by_gh.txt) <(sort found_by_git.txt) | sed 's=^= =' | tr -d '()')" -printf $'\n---\nReports\n\n' +printf $'\n```spoiler Reports\n\n' if [ -z "${only_gh}" ] then @@ -93,6 +123,6 @@ else printf $'\n* PRs not found by `gh` (merged by %s, closed after %s?)\n%s\n' "${endDate}" "${endDate}" "${only_git}" fi -printf -- $'---\n' +printf -- $'```\n' rm -rf found_by_gh.txt found_by_git.txt From a48210ea6bd8c90c2b58af2e472ac30d899a4f82 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Sun, 18 Jan 2026 16:28:41 +0100 Subject: [PATCH 188/191] avoid temporary files --- scripts/find_labels.sh | 33 ++++++++++++++++++++------------- 1 file changed, 20 insertions(+), 13 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index bb16a2c7f32965..7805281e7d6a46 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -20,8 +20,6 @@ if [ "$#" -ne 3 ]; then exit 1 fi -rm -rf found_by_gh.txt found_by_git.txt - repository="${1}" # Get the start and end dates @@ -37,13 +35,6 @@ prs=$(gh pr list --repo "$repository" --state closed --base master --search "clo ## Print PR numbers, their labels and their title #echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Title: \(.title)"' -# Store to file `found_by_gh.txt` the PR numbers, as found by `gh` -echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "(#\(.number))"' | sort >> found_by_gh.txt - -# Store to file `found_by_git.txt` the PR numbers, as found by looking at the commits to `master` -git log --pretty=oneline --since="${startDate}" --until="${endDate}" | - sed -n 's=.*\((#[0-9]*)\)$=\1=p' | sort >> found_by_git.txt - commits_in_range="$(git log --since="${startDate}" --until="${endDate}" --pretty=oneline | wc -l)" printf $'\n\nBetween %s and %s there were\n' "${startDate}" "${endDate/%T*}" @@ -104,8 +95,26 @@ formatForZulip () { formatForZulip "${formattedPRs}" -only_gh="$( comm -23 <(sort found_by_gh.txt) <(sort found_by_git.txt) | sed 's=^= =' | tr -d '()')" -only_git="$(comm -13 <(sort found_by_gh.txt) <(sort found_by_git.txt) | sed 's=^= =' | tr -d '()')" +# Store to variable `found_by_gh` the PR numbers, as found by `gh` +found_by_gh="$( + echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "(#\(.number))"' | sort -u +)" + +# Store to variable `found_by_git` the PR numbers, as found by looking at the commits to `master` +found_by_git="$( + git log --pretty=oneline --since="${startDate}" --until="${endDate}" | + sed -n 's=.*\((#[0-9]*)\)$=\1=p' | sort -u +)" + +only_gh="$( + comm -23 <(printf $'%s\n' "${found_by_gh}") <(printf $'%s\n' "${found_by_git}") | + sed 's=^= =' | tr -d '()' +)" + +only_git="$( + comm -13 <(printf $'%s\n' "${found_by_gh}") <(printf $'%s\n' "${found_by_git}") | + sed 's=^= =' | tr -d '()' +)" printf $'\n```spoiler Reports\n\n' @@ -124,5 +133,3 @@ else fi printf -- $'```\n' - -rm -rf found_by_gh.txt found_by_git.txt From 628e4cbb66713ff75193807b2f76e5de3b6e8b62 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Sun, 18 Jan 2026 22:50:17 +0100 Subject: [PATCH 189/191] prune --- scripts/find_labels.sh | 5 ----- 1 file changed, 5 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 7805281e7d6a46..57971a0f322632 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -32,11 +32,6 @@ commits_in_range="$(git log --since="${startDate}" --until="${endDate}" --pretty # Retrieve merged PRs from the given range prs=$(gh pr list --repo "$repository" --state closed --base master --search "closed:${startDate}..${endDate}" --json number,labels,title,author --limit "$((commits_in_range * 2))") -## Print PR numbers, their labels and their title -#echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Title: \(.title)"' - -commits_in_range="$(git log --since="${startDate}" --until="${endDate}" --pretty=oneline | wc -l)" - printf $'\n\nBetween %s and %s there were\n' "${startDate}" "${endDate/%T*}" printf $'* %s commits to `master` and\n' "${commits_in_range}" From a6527c4ec2df4a0a326c7057cdec13dc99b3661f Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Sun, 18 Jan 2026 23:05:52 +0100 Subject: [PATCH 190/191] add forZulip flag, rearrange --- scripts/find_labels.sh | 38 +++++++++++++++++++++++--------------- 1 file changed, 23 insertions(+), 15 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index 57971a0f322632..adaaa76d16142e 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -20,6 +20,7 @@ if [ "$#" -ne 3 ]; then exit 1 fi +forZulip=true repository="${1}" # Get the start and end dates @@ -88,8 +89,6 @@ formatForZulip () { ' } -formatForZulip "${formattedPRs}" - # Store to variable `found_by_gh` the PR numbers, as found by `gh` found_by_gh="$( echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "(#\(.number))"' | sort -u @@ -111,20 +110,29 @@ only_git="$( sed 's=^= =' | tr -d '()' )" -printf $'\n```spoiler Reports\n\n' - -if [ -z "${only_gh}" ] -then - printf $'* All PRs are accounted for!\n' -else - printf $'* PRs not corresponding to a commit (merged before %s, closed on %s?)\n%s\n' "${startDate}" "${startDate}" "${only_gh}" -fi +reports="$( + if [ -z "${only_gh}" ] + then + printf $'* All PRs are accounted for!\n' + else + printf $'* PRs not corresponding to a commit (merged before %s, closed on %s?)\n%s\n' "${startDate}" "${startDate}" "${only_gh}" + fi + + if [ -z "${only_git}" ] + then + printf $'\n* All commits are accounted for!\n' + else + printf $'\n* PRs not found by `gh` (merged by %s, closed after %s?)\n%s\n' "${endDate}" "${endDate}" "${only_git}" + fi +)" -if [ -z "${only_git}" ] +if [ "${forZulip}" == "true" ] then - printf $'\n* All commits are accounted for!\n' + formatForZulip "${formattedPRs}" + printf $'\n```spoiler Reports\n\n%s\n' "${reports}" + printf -- $'```\n' else - printf $'\n* PRs not found by `gh` (merged by %s, closed after %s?)\n%s\n' "${endDate}" "${endDate}" "${only_git}" + formatForGitHub "${formattedPRs}" + printf $'
\n\n
Reports\n\n%s\n' "${reports}" + printf $'
\n' fi - -printf -- $'```\n' From 84c201a2d796637a92869e060637777c56630b02 Mon Sep 17 00:00:00 2001 From: Damiano Testa Date: Sun, 18 Jan 2026 23:14:19 +0100 Subject: [PATCH 191/191] more formatting --- scripts/find_labels.sh | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh index adaaa76d16142e..5f56c8df13bc95 100755 --- a/scripts/find_labels.sh +++ b/scripts/find_labels.sh @@ -33,10 +33,6 @@ commits_in_range="$(git log --since="${startDate}" --until="${endDate}" --pretty # Retrieve merged PRs from the given range prs=$(gh pr list --repo "$repository" --state closed --base master --search "closed:${startDate}..${endDate}" --json number,labels,title,author --limit "$((commits_in_range * 2))") -printf $'\n\nBetween %s and %s there were\n' "${startDate}" "${endDate/%T*}" - -printf $'* %s commits to `master` and\n' "${commits_in_range}" - formattedPRs="$(echo "$prs" | jq -S -r '.[] | select(.title | startswith("[Merged by Bors]")) | @@ -126,6 +122,12 @@ reports="$( fi )" +printf $'### Commits to `%s` between %s and %s\n' "$(basename "${repository}")" "${startDate//T*/}" "${endDate//T*/}" + +printf $'\n\nBetween %s and %s there were\n' "${startDate}" "${endDate/%T*}" + +printf $'* %s commits to `master` and\n' "${commits_in_range}" + if [ "${forZulip}" == "true" ] then formatForZulip "${formattedPRs}"