From 94d182de84afc4154afa4ea2583a0f1a0a9b4bdc Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 09:28:23 +0200 Subject: [PATCH 01/65] add script and action for monthly PR summary --- .github/workflows/monthly_pr_report.yaml | 56 +++++++++++++ monthly_summary.sh | 102 +++++++++++++++++++++++ 2 files changed, 158 insertions(+) create mode 100644 .github/workflows/monthly_pr_report.yaml create mode 100755 monthly_summary.sh diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml new file mode 100644 index 00000000..8070a9da --- /dev/null +++ b/.github/workflows/monthly_pr_report.yaml @@ -0,0 +1,56 @@ +on: + pull_request + +name: Blog report + +jobs: + + Monthly_PRs: + if: github.event.pull_request.draft == false + name: Blog draft + runs-on: ubuntu-latest + + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + MATHLIB: leanprover-community/mathlib4 + + steps: + - name: cleanup + run: | + find . -name . -o -prune -exec rm -rf -- {} + + + - uses: actions/checkout@v4 + with: + path: blog + + - uses: actions/checkout@v4 + with: + repository: "${MATHLIB}" + fetch-depth: 0 + ref: master + path: mathlib + + - name: blog report + run: | + yrMth=2024-07 + mth="$(date -d "${yrMth}-01" '+%B')" + PR="${{ github.event.pull_request.number }}" + title="### ${mth} in Mathlib summary" + + #git checkout origin/adomani/yd_find_label monthly_summary.sh + message="$(printf '%s\n\n%s\n' "${title}" "$(cd mathlib; ./../blog/monthly_summary.sh "${MATHLIB}" "${yrMth}")")" + echo "${message}" + baseUrl="https://github.com/${MATHLIB}/pull" + message="$(echo "${message}" | + sed ' + / [0-9]* PRs$/{ + s=^=
\n= + s=$=\n\n= + } + s=^PR #\([0-9]*\)=* PR [#\1]('"${baseUrl}"'\1)=' | + sed -z ' + s=
=
= + s=\n---\nReports\n\n=\n
\n\n---\n\n
Reports\n\n= + s=\n---[\n]*$=\n\n
\n&= + ')" + ./mathlib/scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" diff --git a/monthly_summary.sh b/monthly_summary.sh new file mode 100755 index 00000000..92cb69a5 --- /dev/null +++ b/monthly_summary.sh @@ -0,0 +1,102 @@ +#!/bin/bash + +# Check if required arguments are provided +if [ "$#" -ne 2 ]; then + printf $'Usage: %s \n\nFor instance `%s leanprover-community/mathlib4`\n\n' "${0}" "${0}" + exit 1 +fi + +rm -rf found_by_gh.txt found_by_git.txt + +findInRange () { + +repository="${1}" + +# Get the start and end dates +startDate="${2}" +endDate="${3}" + +# find how many commits to master there have been in the last month +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,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)"' + +# 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 + +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" + +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)" + +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}" + +( +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)"' | + sort | + awk 'BEGIN{ labels=""; con=0; total=0 } + { total++ + 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 } + END { + printf("* %s closed PRs\n", total) + for(i=1; i<=con; i++) { + tag=order[i] + gsub(/\[\]/, "Miscellaneous", tag) + gsub(/["\][]/, "", tag) + gsub(/,/, " ", tag) + noPR=seen[order[i]] + printf("\n%s, %s PR%s%s\n", tag, noPR, noPR == "1" ? "" : "s", acc[order[i]]) + } + } + ' + +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' + +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}" +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}" +fi + +printf -- $'---\n' + +rm -rf found_by_gh.txt found_by_git.txt From 3115cff1cc1f822fa120a023f4854bcc3f82cbcb Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 09:30:36 +0200 Subject: [PATCH 02/65] explicit repo --- .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 8070a9da..34a2b2cf 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -25,7 +25,7 @@ jobs: - uses: actions/checkout@v4 with: - repository: "${MATHLIB}" + repository: leanprover-community/mathlib4 fetch-depth: 0 ref: master path: mathlib From e2eb004e60d051fad456e7fe3d579542672e91c8 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 09:32:47 +0200 Subject: [PATCH 03/65] print path --- .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 34a2b2cf..760cf5ce 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -53,4 +53,5 @@ jobs: s=\n---\nReports\n\n=\n
\n\n---\n\n
Reports\n\n= s=\n---[\n]*$=\n\n
\n&= ')" - ./mathlib/scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" + pwd + ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" From 715323e34737d74eb25d625894ad1b0f82c6af99 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 09:37:27 +0200 Subject: [PATCH 04/65] plant info --- .github/workflows/monthly_pr_report.yaml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 760cf5ce..520b826e 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -53,5 +53,12 @@ jobs: s=\n---\nReports\n\n=\n\n\n---\n\n
Reports\n\n= s=\n---[\n]*$=\n\n
\n&= ')" + echo "pwd" pwd - ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" + echo "ls" + ls + cd .. + echo ".. ls" + pwd + ls + ./mathlib/scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" From 225abeee9a1a0e64aa101d0215ba4211a3eaa339 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 09:42:33 +0200 Subject: [PATCH 05/65] show 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 520b826e..cacee7fc 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -57,8 +57,9 @@ jobs: pwd echo "ls" ls - cd .. - echo ".. ls" - pwd + #cd .. + #echo ".. ls" + #pwd ls + cat mathlib/scripts/update_PR_comment.sh ./mathlib/scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" From 05dc150fc313f065673460a9ce49de9104305a09 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 09:46:34 +0200 Subject: [PATCH 06/65] sed -i --- .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 cacee7fc..12e0c301 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -61,5 +61,6 @@ jobs: #echo ".. ls" #pwd ls + sed -i 's=${GITHUB_REPOSITORY}=leanprover-community/blog=' mathlib/scripts/update_PR_comment.sh cat mathlib/scripts/update_PR_comment.sh ./mathlib/scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" From 1af9102bf4f58a2089986dcbdce1900a3cc00f70 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 11:24:31 +0200 Subject: [PATCH 07/65] chmod --- .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 12e0c301..7c96cfc0 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -62,5 +62,6 @@ jobs: #pwd ls sed -i 's=${GITHUB_REPOSITORY}=leanprover-community/blog=' mathlib/scripts/update_PR_comment.sh + chmod u+rx mathlib/scripts/update_PR_comment.sh cat mathlib/scripts/update_PR_comment.sh ./mathlib/scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" From ff1b5f02b2b1fb1bc4e2ffa6b7144a7b033d7873 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 11:27:20 +0200 Subject: [PATCH 08/65] show command --- .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 7c96cfc0..2259726c 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -64,4 +64,5 @@ jobs: sed -i 's=${GITHUB_REPOSITORY}=leanprover-community/blog=' mathlib/scripts/update_PR_comment.sh chmod u+rx mathlib/scripts/update_PR_comment.sh cat mathlib/scripts/update_PR_comment.sh + printf './mathlib/scripts/update_PR_comment.sh %s %s %s\n' "message" "${title}" "${PR}" ./mathlib/scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" From d5a114bdec11c257b1de27293f6eb2ae2863120d Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 11:32:17 +0200 Subject: [PATCH 09/65] show other message --- .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 2259726c..d2667034 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -39,7 +39,7 @@ jobs: #git checkout origin/adomani/yd_find_label monthly_summary.sh message="$(printf '%s\n\n%s\n' "${title}" "$(cd mathlib; ./../blog/monthly_summary.sh "${MATHLIB}" "${yrMth}")")" - echo "${message}" + #echo "${message}" baseUrl="https://github.com/${MATHLIB}/pull" message="$(echo "${message}" | sed ' @@ -53,6 +53,7 @@ jobs: s=\n---\nReports\n\n=\n\n\n---\n\n
Reports\n\n= s=\n---[\n]*$=\n\n
\n&= ')" + echo "${message}" echo "pwd" pwd echo "ls" From d350525cfb8051901a4873ba9dbf822c7d8028a0 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 11:35:39 +0200 Subject: [PATCH 10/65] explicit --- .github/workflows/monthly_pr_report.yaml | 27 ++++++++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index d2667034..ca6ac347 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -66,4 +66,31 @@ jobs: chmod u+rx mathlib/scripts/update_PR_comment.sh cat mathlib/scripts/update_PR_comment.sh printf './mathlib/scripts/update_PR_comment.sh %s %s %s\n' "message" "${title}" "${PR}" + + # the text of the message that will replace the current one + message="${message}" + # the start of the message to locate it among all messages in the PR + comment_init="${title}" + # the PR number + PR="${PR}" + echo "using: '${title}' '${PR}'" + data=$(jq -n --arg msg "$message" '{"body": $msg}') + baseURL="https://api.github.com/repos/leanprover-community/blog/issues" + printf 'Base url: %s\n' "${baseURL}" + method="POST" + if [[ -n "$message" ]]; then + url="${baseURL}/${PR}/comments" + printf 'Base url: %s\n' "${url}" + headers="Authorization: token ${GITHUB_TOKEN}" + comment_id=$(curl -s -S -H "Content-Type: application/json" -H "$headers" "$url" | + jq --arg cID "${comment_init}" -r '.[] | select(.body | startswith($cID)) | .id' | head -1) + echo "Comment id: '${comment_id}'" + if [[ -n "$comment_id" ]]; then + url="${baseURL}/comments/${comment_id}" + method="PATCH" + fi + curl -s -S -H "Content-Type: application/json" -H "$headers" -X "$method" -d "$data" "$url" + fi + + ./mathlib/scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" From 9166c8b0d944045384d653a182da39588fc13b46 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 11:37:42 +0200 Subject: [PATCH 11/65] rename variable message --> mim --- .github/workflows/monthly_pr_report.yaml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index ca6ac347..e8aa7b10 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -38,10 +38,10 @@ jobs: title="### ${mth} in Mathlib summary" #git checkout origin/adomani/yd_find_label monthly_summary.sh - message="$(printf '%s\n\n%s\n' "${title}" "$(cd mathlib; ./../blog/monthly_summary.sh "${MATHLIB}" "${yrMth}")")" - #echo "${message}" + mim="$(printf '%s\n\n%s\n' "${title}" "$(cd mathlib; ./../blog/monthly_summary.sh "${MATHLIB}" "${yrMth}")")" + #echo "${mim}" baseUrl="https://github.com/${MATHLIB}/pull" - message="$(echo "${message}" | + mim="$(echo "${mim}" | sed ' / [0-9]* PRs$/{ s=^=
\n= @@ -53,7 +53,7 @@ jobs: s=\n---\nReports\n\n=\n
\n\n---\n\n
Reports\n\n= s=\n---[\n]*$=\n\n
\n&= ')" - echo "${message}" + echo "${mim}" echo "pwd" pwd echo "ls" @@ -68,7 +68,7 @@ jobs: printf './mathlib/scripts/update_PR_comment.sh %s %s %s\n' "message" "${title}" "${PR}" # the text of the message that will replace the current one - message="${message}" + message="${mim}" # the start of the message to locate it among all messages in the PR comment_init="${title}" # the PR number From 800110ec51f3c1773fa098c382e2252cb4ab1e26 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 11:39:47 +0200 Subject: [PATCH 12/65] line too long? --- .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 e8aa7b10..aa25ccc1 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -93,4 +93,4 @@ jobs: fi - ./mathlib/scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" + #./mathlib/scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" From 9aaade6f205172a3fb1189cc1bdbae14ef921ed5 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 12:20:35 +0200 Subject: [PATCH 13/65] shorter 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 aa25ccc1..7608d58a 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -93,4 +93,4 @@ jobs: fi - #./mathlib/scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" + #./mathlib/scripts/update_PR_comment.sh "${title} message" "${title}" "${PR}" From 055aa142f7b4ea9a4f3edb575985d80b1b8c1870 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 12:23:43 +0200 Subject: [PATCH 14/65] show data --- .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 7608d58a..cac6a4f8 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -75,6 +75,7 @@ jobs: PR="${PR}" echo "using: '${title}' '${PR}'" data=$(jq -n --arg msg "$message" '{"body": $msg}') + echo "$data" baseURL="https://api.github.com/repos/leanprover-community/blog/issues" printf 'Base url: %s\n' "${baseURL}" method="POST" From ccc8d2396d08724b7800ff3707c56ba4837523a6 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 12:25:33 +0200 Subject: [PATCH 15/65] no data --- .github/workflows/monthly_pr_report.yaml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index cac6a4f8..534b4a45 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -74,8 +74,9 @@ jobs: # the PR number PR="${PR}" echo "using: '${title}' '${PR}'" - data=$(jq -n --arg msg "$message" '{"body": $msg}') - echo "$data" + #data=$(jq -n --arg msg "$message" '{"body": $msg}') + echo "data: ${data}" + man jq baseURL="https://api.github.com/repos/leanprover-community/blog/issues" printf 'Base url: %s\n' "${baseURL}" method="POST" From 97ec4826d3186e56ffea8d8d55a786a29ef583e3 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 12:32:26 +0200 Subject: [PATCH 16/65] shorter text, shallow clone --- .github/workflows/monthly_pr_report.yaml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 534b4a45..e44c5138 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -26,7 +26,7 @@ jobs: - uses: actions/checkout@v4 with: repository: leanprover-community/mathlib4 - fetch-depth: 0 + #fetch-depth: 0 ref: master path: mathlib @@ -38,7 +38,8 @@ jobs: title="### ${mth} in Mathlib summary" #git checkout origin/adomani/yd_find_label monthly_summary.sh - mim="$(printf '%s\n\n%s\n' "${title}" "$(cd mathlib; ./../blog/monthly_summary.sh "${MATHLIB}" "${yrMth}")")" + #mim="$(printf '%s\n\n%s\n' "${title}" "$(cd mathlib; ./../blog/monthly_summary.sh "${MATHLIB}" "${yrMth}")")" + mim="${title} and something else" #echo "${mim}" baseUrl="https://github.com/${MATHLIB}/pull" mim="$(echo "${mim}" | From 4a47cfc02660a352a0c34a544c89b837ea1552c5 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 12:33:14 +0200 Subject: [PATCH 17/65] no man jq --- .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 e44c5138..90acb6a2 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -77,7 +77,7 @@ jobs: echo "using: '${title}' '${PR}'" #data=$(jq -n --arg msg "$message" '{"body": $msg}') echo "data: ${data}" - man jq + #man jq baseURL="https://api.github.com/repos/leanprover-community/blog/issues" printf 'Base url: %s\n' "${baseURL}" method="POST" @@ -96,4 +96,4 @@ jobs: fi - #./mathlib/scripts/update_PR_comment.sh "${title} message" "${title}" "${PR}" + ./mathlib/scripts/update_PR_comment.sh "${title} message" "${title}" "${PR}" From 420eaefac287430900dc6eb52bca25398d33e049 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 12:36:47 +0200 Subject: [PATCH 18/65] echos --- .github/workflows/monthly_pr_report.yaml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 90acb6a2..a7b7d973 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -95,5 +95,6 @@ jobs: curl -s -S -H "Content-Type: application/json" -H "$headers" -X "$method" -d "$data" "$url" fi - - ./mathlib/scripts/update_PR_comment.sh "${title} message" "${title}" "${PR}" + echo "running script" + ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" && + echo "after script" From b546c2a92ee8aed7dd1d512581888768cf8871ce Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 12:39:07 +0200 Subject: [PATCH 19/65] mathlib --- .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 a7b7d973..4a334162 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -96,5 +96,5 @@ jobs: fi echo "running script" - ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" && + ./mathlib/scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" && echo "after script" From b8458c6c2de114304260cba2db3d46cac000a680 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 12:43:25 +0200 Subject: [PATCH 20/65] use hello --- .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 4a334162..a123d880 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -75,7 +75,7 @@ jobs: # the PR number PR="${PR}" echo "using: '${title}' '${PR}'" - #data=$(jq -n --arg msg "$message" '{"body": $msg}') + data=$(jq -n --arg msg "hello" '{"body": $msg}') # "$message" '{"body": $msg}') echo "data: ${data}" #man jq baseURL="https://api.github.com/repos/leanprover-community/blog/issues" From df75f778f0c0ebf57bf588a936129fe119f0568f Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 13:04:18 +0200 Subject: [PATCH 21/65] here or there --- .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 a123d880..2afb015e 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -90,8 +90,10 @@ jobs: echo "Comment id: '${comment_id}'" if [[ -n "$comment_id" ]]; then url="${baseURL}/comments/${comment_id}" + echo "are we here?" method="PATCH" fi + echo "or are we there?" curl -s -S -H "Content-Type: application/json" -H "$headers" -X "$method" -d "$data" "$url" fi From 56653679a1f1698a3f120443f6145222f72a6d83 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 13:14:42 +0200 Subject: [PATCH 22/65] copy paste comment action --- .github/workflows/monthly_pr_report.yaml | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 2afb015e..b2af9067 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -19,6 +19,16 @@ jobs: run: | find . -name . -o -prune -exec rm -rf -- {} + + - uses: actions/github-script@v6 + with: + script: | + github.rest.issues.createComment({ + issue_number: context.issue.number, + owner: context.repo.owner, + repo: context.repo.repo, + body: '👋 Thanks for reporting!' + }) + - uses: actions/checkout@v4 with: path: blog From fdac0cabaf4579b884464705dd0fd264bb64d433 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 13:16:42 +0200 Subject: [PATCH 23/65] add permissions --- .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 b2af9067..ed705309 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -9,6 +9,7 @@ jobs: if: github.event.pull_request.draft == false name: Blog draft runs-on: ubuntu-latest + permissions: write-all env: GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} From 3fa061c925468354df43bcb89da27028a637780c Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 13:35:10 +0200 Subject: [PATCH 24/65] different permissions --- .github/workflows/monthly_pr_report.yaml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index ed705309..a908ca06 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -9,7 +9,10 @@ jobs: if: github.event.pull_request.draft == false name: Blog draft runs-on: ubuntu-latest - permissions: write-all + permissions: + contents: write + pull-requests: write + repository-projects: write env: GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} From 498d24564f6f2a7fec2b7341d4142646ae87c117 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 13:37:39 +0200 Subject: [PATCH 25/65] add actionlint --- .github/actionlint.yml | 4 ++++ .github/workflows/actionlint.yml | 20 ++++++++++++++++++++ 2 files changed, 24 insertions(+) create mode 100644 .github/actionlint.yml create mode 100644 .github/workflows/actionlint.yml diff --git a/.github/actionlint.yml b/.github/actionlint.yml new file mode 100644 index 00000000..9135c9bb --- /dev/null +++ b/.github/actionlint.yml @@ -0,0 +1,4 @@ +self-hosted-runner: + labels: + - bors + - pr diff --git a/.github/workflows/actionlint.yml b/.github/workflows/actionlint.yml new file mode 100644 index 00000000..dd9a83c5 --- /dev/null +++ b/.github/workflows/actionlint.yml @@ -0,0 +1,20 @@ +name: Actionlint +on: + push: + branches: + - 'master' + paths: + - '.github/**' + pull_request: + paths: + - '.github/**' + merge_group: + +jobs: + actionlint: + runs-on: ubuntu-latest + steps: + - name: Checkout + uses: actions/checkout@v4 + - name: actionlint + uses: raven-actions/actionlint@v1 From 0843cecc1f297c5f21ea636afdbf30f5c696ec3f Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 13:41:21 +0200 Subject: [PATCH 26/65] update versions --- .github/workflows/build.yml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 1e48fadc..a728e5e9 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -12,18 +12,18 @@ jobs: name: Build HTML runs-on: ubuntu-latest steps: - - uses: actions/checkout@v2 + - uses: actions/checkout@v4 - name: install Python - uses: actions/setup-python@v1 + uses: actions/setup-python@v5 with: - python-version: 3.9 + python-version: 3.12 - name: install Python dependencies run: python -m pip install -r requirements.txt - name: build site - run: ./deploy.sh + run: ./deploy.sh env: git_hash: ${{ github.sha }} DEPLOY_GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} From ac8175c3f8600431901295775e32306b2542cf0d Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 13:44:00 +0200 Subject: [PATCH 27/65] mim1 --- .github/workflows/monthly_pr_report.yaml | 14 ++------------ 1 file changed, 2 insertions(+), 12 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index a908ca06..36ae304f 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -53,10 +53,10 @@ jobs: #git checkout origin/adomani/yd_find_label monthly_summary.sh #mim="$(printf '%s\n\n%s\n' "${title}" "$(cd mathlib; ./../blog/monthly_summary.sh "${MATHLIB}" "${yrMth}")")" - mim="${title} and something else" + mim1="${title} and something else" #echo "${mim}" baseUrl="https://github.com/${MATHLIB}/pull" - mim="$(echo "${mim}" | + mim="$(echo "${mim1}" | sed ' / [0-9]* PRs$/{ s=^=
\n= @@ -68,19 +68,9 @@ jobs: s=\n---\nReports\n\n=\n
\n\n---\n\n
Reports\n\n= s=\n---[\n]*$=\n\n
\n&= ')" - echo "${mim}" - echo "pwd" - pwd - echo "ls" - ls - #cd .. - #echo ".. ls" - #pwd - ls sed -i 's=${GITHUB_REPOSITORY}=leanprover-community/blog=' mathlib/scripts/update_PR_comment.sh chmod u+rx mathlib/scripts/update_PR_comment.sh cat mathlib/scripts/update_PR_comment.sh - printf './mathlib/scripts/update_PR_comment.sh %s %s %s\n' "message" "${title}" "${PR}" # the text of the message that will replace the current one message="${mim}" From f18d295322e1b8b2281cfdd23763c07d982a56d4 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 13:46:07 +0200 Subject: [PATCH 28/65] unassign --- .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 36ae304f..dd20a94e 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -77,7 +77,7 @@ jobs: # the start of the message to locate it among all messages in the PR comment_init="${title}" # the PR number - PR="${PR}" + #PR="${PR}" echo "using: '${title}' '${PR}'" data=$(jq -n --arg msg "hello" '{"body": $msg}') # "$message" '{"body": $msg}') echo "data: ${data}" From 2ede39688b6a48a29d78d4c1b5bf823ec513b8a3 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 13:46:52 +0200 Subject: [PATCH 29/65] lint? --- .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 dd20a94e..034ada99 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -68,7 +68,7 @@ jobs: s=\n---\nReports\n\n=\n\n\n---\n\n
Reports\n\n= s=\n---[\n]*$=\n\n
\n&= ')" - sed -i 's=${GITHUB_REPOSITORY}=leanprover-community/blog=' mathlib/scripts/update_PR_comment.sh + sed -i 's=$'"{GITHUB_REPOSITORY}"''=leanprover-community/blog=' mathlib/scripts/update_PR_comment.sh chmod u+rx mathlib/scripts/update_PR_comment.sh cat mathlib/scripts/update_PR_comment.sh From f6ea1836e38dcfef4a80845be2eb252aa10179a6 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 13:48:49 +0200 Subject: [PATCH 30/65] escape --- .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 034ada99..036adae7 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -68,7 +68,7 @@ jobs: s=\n---\nReports\n\n=\n\n\n---\n\n
Reports\n\n= s=\n---[\n]*$=\n\n
\n&= ')" - sed -i 's=$'"{GITHUB_REPOSITORY}"''=leanprover-community/blog=' mathlib/scripts/update_PR_comment.sh + sed -i "s=\${GITHUB_REPOSITORY}=leanprover-community/blog=" mathlib/scripts/update_PR_comment.sh chmod u+rx mathlib/scripts/update_PR_comment.sh cat mathlib/scripts/update_PR_comment.sh From 68edcc8e3741fe558758dcfe5ab01f71c096a354 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 13:54:11 +0200 Subject: [PATCH 31/65] add token to script --- .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 036adae7..802dcea3 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -25,6 +25,7 @@ jobs: - uses: actions/github-script@v6 with: + github-token: ${{ secrets.GITHUB_TOKEN }} script: | github.rest.issues.createComment({ issue_number: context.issue.number, From bfeec91e1130bfbe12ed3491e0dce50810cf1f93 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 15:11:57 +0200 Subject: [PATCH 32/65] summary --- .github/workflows/monthly_pr_report.yaml | 30 +++++++++++++++--------- 1 file changed, 19 insertions(+), 11 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 802dcea3..b6ac6691 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -23,17 +23,6 @@ jobs: run: | find . -name . -o -prune -exec rm -rf -- {} + - - uses: actions/github-script@v6 - with: - github-token: ${{ secrets.GITHUB_TOKEN }} - script: | - github.rest.issues.createComment({ - issue_number: context.issue.number, - owner: context.repo.owner, - repo: context.repo.repo, - body: '👋 Thanks for reporting!' - }) - - uses: actions/checkout@v4 with: path: blog @@ -86,6 +75,8 @@ jobs: baseURL="https://api.github.com/repos/leanprover-community/blog/issues" printf 'Base url: %s\n' "${baseURL}" method="POST" + printf '### Summary\n\n' > "${GITHUB_STEP_SUMMARY}" + #./scripts/no_lost_declarations.sh >> "${GITHUB_STEP_SUMMARY}" if [[ -n "$message" ]]; then url="${baseURL}/${PR}/comments" printf 'Base url: %s\n' "${url}" @@ -105,3 +96,20 @@ jobs: echo "running script" ./mathlib/scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" && echo "after script" + #name: print_lost_declarations + #run: | + ## back and forth to settle a "detached head" (maybe?) + #git checkout -q master + #git checkout -q - + + + - uses: actions/github-script@v6 + with: + github-token: ${{ secrets.GITHUB_TOKEN }} + script: | + github.rest.issues.createComment({ + issue_number: context.issue.number, + owner: context.repo.owner, + repo: context.repo.repo, + body: '👋 Thanks for reporting!' + }) From 967f99675626242291eb6f4e0ed7115479ce954d Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 15:13:18 +0200 Subject: [PATCH 33/65] remove last step --- .github/workflows/monthly_pr_report.yaml | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index b6ac6691..b27b54cd 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -101,15 +101,3 @@ jobs: ## back and forth to settle a "detached head" (maybe?) #git checkout -q master #git checkout -q - - - - - uses: actions/github-script@v6 - with: - github-token: ${{ secrets.GITHUB_TOKEN }} - script: | - github.rest.issues.createComment({ - issue_number: context.issue.number, - owner: context.repo.owner, - repo: context.repo.repo, - body: '👋 Thanks for reporting!' - }) From 8b80dc4b4c07373fa51eee85cb1d732da09d47c8 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 15:15:16 +0200 Subject: [PATCH 34/65] more summary --- .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 b27b54cd..e5f668e8 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -75,7 +75,7 @@ jobs: baseURL="https://api.github.com/repos/leanprover-community/blog/issues" printf 'Base url: %s\n' "${baseURL}" method="POST" - printf '### Summary\n\n' > "${GITHUB_STEP_SUMMARY}" + printf '%s\n' "${mim}" > "${GITHUB_STEP_SUMMARY}" #./scripts/no_lost_declarations.sh >> "${GITHUB_STEP_SUMMARY}" if [[ -n "$message" ]]; then url="${baseURL}/${PR}/comments" From 605059b2fb6692004e7e5e897150cf43e74db206 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 15:16:25 +0200 Subject: [PATCH 35/65] full output --- .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 e5f668e8..bcb03804 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -42,8 +42,8 @@ jobs: title="### ${mth} in Mathlib summary" #git checkout origin/adomani/yd_find_label monthly_summary.sh - #mim="$(printf '%s\n\n%s\n' "${title}" "$(cd mathlib; ./../blog/monthly_summary.sh "${MATHLIB}" "${yrMth}")")" - mim1="${title} and something else" + mim1="$(printf '%s\n\n%s\n' "${title}" "$(cd mathlib; ./../blog/monthly_summary.sh "${MATHLIB}" "${yrMth}")")" + #mim1="${title} and something else" #echo "${mim}" baseUrl="https://github.com/${MATHLIB}/pull" mim="$(echo "${mim1}" | From 880a87c978cfc75ecae810fa4bd70f805699472e Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 15:17:20 +0200 Subject: [PATCH 36/65] fetch all --- .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 bcb03804..de4d4ddb 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -30,7 +30,7 @@ jobs: - uses: actions/checkout@v4 with: repository: leanprover-community/mathlib4 - #fetch-depth: 0 + fetch-depth: 0 ref: master path: mathlib From 6fa92da9779d5133531794991fe7e6b7980be5a5 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 15:19:43 +0200 Subject: [PATCH 37/65] slash --- .github/workflows/monthly_pr_report.yaml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index de4d4ddb..9db821c6 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -45,7 +45,7 @@ jobs: mim1="$(printf '%s\n\n%s\n' "${title}" "$(cd mathlib; ./../blog/monthly_summary.sh "${MATHLIB}" "${yrMth}")")" #mim1="${title} and something else" #echo "${mim}" - baseUrl="https://github.com/${MATHLIB}/pull" + baseUrl="https://github.com/${MATHLIB}/pull/" mim="$(echo "${mim1}" | sed ' / [0-9]* PRs$/{ @@ -93,9 +93,9 @@ jobs: curl -s -S -H "Content-Type: application/json" -H "$headers" -X "$method" -d "$data" "$url" fi - echo "running script" - ./mathlib/scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" && - echo "after script" + #echo "running script" + #./mathlib/scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" && + # echo "after script" #name: print_lost_declarations #run: | ## back and forth to settle a "detached head" (maybe?) From 1ee940e5ff2d4251ec3bf16c6251fcc254f2131a Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 15:23:29 +0200 Subject: [PATCH 38/65] PR all and cleanup --- .github/workflows/monthly_pr_report.yaml | 42 ------------------------ monthly_summary.sh | 4 +-- 2 files changed, 2 insertions(+), 44 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 9db821c6..bac5b097 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -58,46 +58,4 @@ jobs: s=\n---\nReports\n\n=\n\n\n---\n\n
Reports\n\n= s=\n---[\n]*$=\n\n
\n&= ')" - sed -i "s=\${GITHUB_REPOSITORY}=leanprover-community/blog=" mathlib/scripts/update_PR_comment.sh - chmod u+rx mathlib/scripts/update_PR_comment.sh - cat mathlib/scripts/update_PR_comment.sh - - # the text of the message that will replace the current one - message="${mim}" - # the start of the message to locate it among all messages in the PR - comment_init="${title}" - # the PR number - #PR="${PR}" - echo "using: '${title}' '${PR}'" - data=$(jq -n --arg msg "hello" '{"body": $msg}') # "$message" '{"body": $msg}') - echo "data: ${data}" - #man jq - baseURL="https://api.github.com/repos/leanprover-community/blog/issues" - printf 'Base url: %s\n' "${baseURL}" - method="POST" printf '%s\n' "${mim}" > "${GITHUB_STEP_SUMMARY}" - #./scripts/no_lost_declarations.sh >> "${GITHUB_STEP_SUMMARY}" - if [[ -n "$message" ]]; then - url="${baseURL}/${PR}/comments" - printf 'Base url: %s\n' "${url}" - headers="Authorization: token ${GITHUB_TOKEN}" - comment_id=$(curl -s -S -H "Content-Type: application/json" -H "$headers" "$url" | - jq --arg cID "${comment_init}" -r '.[] | select(.body | startswith($cID)) | .id' | head -1) - echo "Comment id: '${comment_id}'" - if [[ -n "$comment_id" ]]; then - url="${baseURL}/comments/${comment_id}" - echo "are we here?" - method="PATCH" - fi - echo "or are we there?" - curl -s -S -H "Content-Type: application/json" -H "$headers" -X "$method" -d "$data" "$url" - fi - - #echo "running script" - #./mathlib/scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" && - # echo "after script" - #name: print_lost_declarations - #run: | - ## back and forth to settle a "detached head" (maybe?) - #git checkout -q master - #git checkout -q - diff --git a/monthly_summary.sh b/monthly_summary.sh index 92cb69a5..d67670d5 100755 --- a/monthly_summary.sh +++ b/monthly_summary.sh @@ -78,8 +78,8 @@ findInRange "${1}" "${yr_mth}-16T00:00:00" "${end_date}" | sed -z 's=^\[==' } ' -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 '()')" +only_gh="$( comm -23 <(sort found_by_gh.txt) <(sort found_by_git.txt) | sed 's=^=* PR =' | tr -d '()')" +only_git="$(comm -13 <(sort found_by_gh.txt) <(sort found_by_git.txt) | sed 's=^=* PR =' | tr -d '()')" printf $'\n---\nReports\n\n' From b26d4ce0bd712a1032ba287c602066ccf0fc1377 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 15:26:07 +0200 Subject: [PATCH 39/65] PRs really and comment unused variable --- .github/workflows/monthly_pr_report.yaml | 3 +-- monthly_summary.sh | 4 ++-- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index bac5b097..feb01795 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -43,8 +43,7 @@ jobs: #git checkout origin/adomani/yd_find_label monthly_summary.sh mim1="$(printf '%s\n\n%s\n' "${title}" "$(cd mathlib; ./../blog/monthly_summary.sh "${MATHLIB}" "${yrMth}")")" - #mim1="${title} and something else" - #echo "${mim}" + echo "${mim}" baseUrl="https://github.com/${MATHLIB}/pull/" mim="$(echo "${mim1}" | sed ' diff --git a/monthly_summary.sh b/monthly_summary.sh index d67670d5..128ff631 100755 --- a/monthly_summary.sh +++ b/monthly_summary.sh @@ -78,8 +78,8 @@ findInRange "${1}" "${yr_mth}-16T00:00:00" "${end_date}" | sed -z 's=^\[==' } ' -only_gh="$( comm -23 <(sort found_by_gh.txt) <(sort found_by_git.txt) | sed 's=^=* PR =' | tr -d '()')" -only_git="$(comm -13 <(sort found_by_gh.txt) <(sort found_by_git.txt) | sed 's=^=* PR =' | tr -d '()')" +only_gh="$( comm -23 <(sort found_by_gh.txt) <(sort found_by_git.txt) | sed 's=^=PR =' | tr -d '()')" +only_git="$(comm -13 <(sort found_by_gh.txt) <(sort found_by_git.txt) | sed 's=^=PR =' | tr -d '()')" printf $'\n---\nReports\n\n' From e03e5719623b391ad72c6d27632d62787d05b267 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 15:27:02 +0200 Subject: [PATCH 40/65] cancel one save and print --- .github/workflows/monthly_pr_report.yaml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index feb01795..10383f04 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -45,7 +45,7 @@ jobs: mim1="$(printf '%s\n\n%s\n' "${title}" "$(cd mathlib; ./../blog/monthly_summary.sh "${MATHLIB}" "${yrMth}")")" echo "${mim}" baseUrl="https://github.com/${MATHLIB}/pull/" - mim="$(echo "${mim1}" | + echo "${mim1}" | sed ' / [0-9]* PRs$/{ s=^=
\n= @@ -56,5 +56,4 @@ jobs: s=
=
= s=\n---\nReports\n\n=\n
\n\n---\n\n
Reports\n\n= s=\n---[\n]*$=\n\n
\n&= - ')" - printf '%s\n' "${mim}" > "${GITHUB_STEP_SUMMARY}" + ' > "${GITHUB_STEP_SUMMARY}" From dbc24eefaf2067f636b526e208d1d28f72c01dd2 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 15:30:52 +0200 Subject: [PATCH 41/65] small cleanup --- .github/workflows/monthly_pr_report.yaml | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 10383f04..4cf9367f 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -9,10 +9,6 @@ jobs: if: github.event.pull_request.draft == false name: Blog draft runs-on: ubuntu-latest - permissions: - contents: write - pull-requests: write - repository-projects: write env: GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} @@ -38,10 +34,9 @@ jobs: run: | yrMth=2024-07 mth="$(date -d "${yrMth}-01" '+%B')" - PR="${{ github.event.pull_request.number }}" + #PR="${{ github.event.pull_request.number }}" title="### ${mth} in Mathlib summary" - #git checkout origin/adomani/yd_find_label monthly_summary.sh mim1="$(printf '%s\n\n%s\n' "${title}" "$(cd mathlib; ./../blog/monthly_summary.sh "${MATHLIB}" "${yrMth}")")" echo "${mim}" baseUrl="https://github.com/${MATHLIB}/pull/" From cfa76868be4dadea59aec390cc7e4e8176708ec5 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 15:33:17 +0200 Subject: [PATCH 42/65] use `mim` --- .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 4cf9367f..3298e58f 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -37,10 +37,10 @@ jobs: #PR="${{ github.event.pull_request.number }}" title="### ${mth} in Mathlib summary" - mim1="$(printf '%s\n\n%s\n' "${title}" "$(cd mathlib; ./../blog/monthly_summary.sh "${MATHLIB}" "${yrMth}")")" + mim="$(printf '%s\n\n%s\n' "${title}" "$(cd mathlib; ./../blog/monthly_summary.sh "${MATHLIB}" "${yrMth}")")" echo "${mim}" baseUrl="https://github.com/${MATHLIB}/pull/" - echo "${mim1}" | + echo "${mim}" | sed ' / [0-9]* PRs$/{ s=^=
\n= From 6c489a87ca0af9b080b56644959f2546ef9ca718 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 15:39:17 +0200 Subject: [PATCH 43/65] reduce number of inputs --- .github/workflows/monthly_pr_report.yaml | 5 ++--- monthly_summary.sh | 10 +++++----- 2 files changed, 7 insertions(+), 8 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 3298e58f..ead4b934 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -12,7 +12,6 @@ jobs: env: GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} - MATHLIB: leanprover-community/mathlib4 steps: - name: cleanup @@ -37,9 +36,9 @@ jobs: #PR="${{ github.event.pull_request.number }}" title="### ${mth} in Mathlib summary" - mim="$(printf '%s\n\n%s\n' "${title}" "$(cd mathlib; ./../blog/monthly_summary.sh "${MATHLIB}" "${yrMth}")")" + mim="$(printf '%s\n\n%s\n' "${title}" "$(cd mathlib; ./../blog/monthly_summary.sh "${yrMth}")")" echo "${mim}" - baseUrl="https://github.com/${MATHLIB}/pull/" + baseUrl="https://github.com/leanprover-community/mathlib4/pull/" echo "${mim}" | sed ' / [0-9]* PRs$/{ diff --git a/monthly_summary.sh b/monthly_summary.sh index 128ff631..ea837414 100755 --- a/monthly_summary.sh +++ b/monthly_summary.sh @@ -1,8 +1,8 @@ #!/bin/bash # Check if required arguments are provided -if [ "$#" -ne 2 ]; then - printf $'Usage: %s \n\nFor instance `%s leanprover-community/mathlib4`\n\n' "${0}" "${0}" +if [ "$#" -ne 1 ]; then + printf $'Usage: %s \n\nFor instance `%s 2024-07`\n\n' "${0}" "${0}" exit 1 fi @@ -10,11 +10,11 @@ rm -rf found_by_gh.txt found_by_git.txt findInRange () { -repository="${1}" +repository=leanprover-community/mathlib4 # Get the start and end dates -startDate="${2}" -endDate="${3}" +startDate="${1}" +endDate="${2}" # find how many commits to master there have been in the last month commits_in_range="$(git log --since="${startDate}" --until="${endDate}" --pretty=oneline | wc -l)" From bc2584fabc05d0d353fb051938778cbdcd7c2000 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 15:40:56 +0200 Subject: [PATCH 44/65] fix --- monthly_summary.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/monthly_summary.sh b/monthly_summary.sh index ea837414..92cadab3 100755 --- a/monthly_summary.sh +++ b/monthly_summary.sh @@ -36,7 +36,7 @@ echo "$prs" } # the current year and month -yr_mth="${2}" #"$(date +%Y-%m)" +yr_mth="${1}" #"$(date +%Y-%m)" yr_mth_day=${yr_mth}-01 start_date="${yr_mth_day}T00:00:00" From b40beeac919b4413a8df61ebe2d7d68bb86fc0f5 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 15:46:06 +0200 Subject: [PATCH 45/65] print dates --- monthly_summary.sh | 3 +++ 1 file changed, 3 insertions(+) diff --git a/monthly_summary.sh b/monthly_summary.sh index 92cadab3..03ab4e31 100755 --- a/monthly_summary.sh +++ b/monthly_summary.sh @@ -16,6 +16,9 @@ repository=leanprover-community/mathlib4 startDate="${1}" endDate="${2}" +echo "startDate: ${startDate}" +echo "endDate: ${endDate}" + # find how many commits to master there have been in the last month commits_in_range="$(git log --since="${startDate}" --until="${endDate}" --pretty=oneline | wc -l)" From 70a83aea5ca9d857b968f1835c3affa70a35c97e Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 15:49:56 +0200 Subject: [PATCH 46/65] limit to 1000 --- monthly_summary.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/monthly_summary.sh b/monthly_summary.sh index 03ab4e31..ad12ca4d 100755 --- a/monthly_summary.sh +++ b/monthly_summary.sh @@ -20,10 +20,10 @@ echo "startDate: ${startDate}" echo "endDate: ${endDate}" # find how many commits to master there have been in the last month -commits_in_range="$(git log --since="${startDate}" --until="${endDate}" --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:${startDate}..${endDate}" --json number,labels,title,author --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 1000) #"$((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 169330e5284fb960a858f6e2f332448230223d6e Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 15:53:51 +0200 Subject: [PATCH 47/65] show dates --- monthly_summary.sh | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/monthly_summary.sh b/monthly_summary.sh index ad12ca4d..72f3d4ba 100755 --- a/monthly_summary.sh +++ b/monthly_summary.sh @@ -16,9 +16,6 @@ repository=leanprover-community/mathlib4 startDate="${1}" endDate="${2}" -echo "startDate: ${startDate}" -echo "endDate: ${endDate}" - # find how many commits to master there have been in the last month #commits_in_range="$(git log --since="${startDate}" --until="${endDate}" --pretty=oneline | wc -l)" @@ -55,6 +52,9 @@ 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}" +echo "First run: ${start_date} ${yr_mth}-15T23:59:59" +echo "Second run: ${yr_mth}-16T00:00:00 ${end_date}" + ( 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=^\[==' From 4b1b6c235ad7b10583c3e97717141399cb242dc1 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 15:56:10 +0200 Subject: [PATCH 48/65] smaller limit --- monthly_summary.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/monthly_summary.sh b/monthly_summary.sh index 72f3d4ba..384b2231 100755 --- a/monthly_summary.sh +++ b/monthly_summary.sh @@ -20,7 +20,7 @@ endDate="${2}" #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,author --limit 1000) #"$((commits_in_range * 2))") +prs=$(gh pr list --repo "$repository" --state closed --base master --search "closed:${startDate}..${endDate}" --json number,labels,title,author --limit 500) #"$((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 7e806b18fa1f4f95259cbfbe4ef15c005c2bfd10 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 15:58:11 +0200 Subject: [PATCH 49/65] ticks --- monthly_summary.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/monthly_summary.sh b/monthly_summary.sh index 384b2231..6f29f2a1 100755 --- a/monthly_summary.sh +++ b/monthly_summary.sh @@ -10,7 +10,7 @@ rm -rf found_by_gh.txt found_by_git.txt findInRange () { -repository=leanprover-community/mathlib4 +repository='leanprover-community/mathlib4' # Get the start and end dates startDate="${1}" From f602146a1f12c7ea93010a16c497b958445df381 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 16:07:38 +0200 Subject: [PATCH 50/65] reduce one input in internal function --- monthly_summary.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/monthly_summary.sh b/monthly_summary.sh index 6f29f2a1..bf9a9e71 100755 --- a/monthly_summary.sh +++ b/monthly_summary.sh @@ -56,8 +56,8 @@ echo "First run: ${start_date} ${yr_mth}-15T23:59:59" echo "Second run: ${yr_mth}-16T00:00:00 ${end_date}" ( -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=^\[==' +findInRange "${start_date}" "${yr_mth}-15T23:59:59" | sed -z 's=]\n*$=,\n=' +findInRange "${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)"' | From 66737414a77359ac3254f10b7c22349792781172 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 16:09:51 +0200 Subject: [PATCH 51/65] restore limit --- monthly_summary.sh | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/monthly_summary.sh b/monthly_summary.sh index bf9a9e71..a713e10e 100755 --- a/monthly_summary.sh +++ b/monthly_summary.sh @@ -17,10 +17,10 @@ startDate="${1}" endDate="${2}" # find how many commits to master there have been in the last month -#commits_in_range="$(git log --since="${startDate}" --until="${endDate}" --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:${startDate}..${endDate}" --json number,labels,title,author --limit 500) #"$((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)"' @@ -52,8 +52,8 @@ 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}" -echo "First run: ${start_date} ${yr_mth}-15T23:59:59" -echo "Second run: ${yr_mth}-16T00:00:00 ${end_date}" +#echo "First run: ${start_date} ${yr_mth}-15T23:59:59" +#echo "Second run: ${yr_mth}-16T00:00:00 ${end_date}" ( findInRange "${start_date}" "${yr_mth}-15T23:59:59" | sed -z 's=]\n*$=,\n=' From e453c378b965ce1a9d287f9a20d0fb0fb134c723 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 16:20:13 +0200 Subject: [PATCH 52/65] improve docs, remove one comment --- .github/workflows/monthly_pr_report.yaml | 1 - monthly_summary.sh | 14 ++++---------- 2 files changed, 4 insertions(+), 11 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index ead4b934..3b4d0ede 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -33,7 +33,6 @@ jobs: run: | yrMth=2024-07 mth="$(date -d "${yrMth}-01" '+%B')" - #PR="${{ github.event.pull_request.number }}" title="### ${mth} in Mathlib summary" mim="$(printf '%s\n\n%s\n' "${title}" "$(cd mathlib; ./../blog/monthly_summary.sh "${yrMth}")")" diff --git a/monthly_summary.sh b/monthly_summary.sh index a713e10e..8b4570b8 100755 --- a/monthly_summary.sh +++ b/monthly_summary.sh @@ -1,6 +1,6 @@ #!/bin/bash -# Check if required arguments are provided +# Check if required argument is provided if [ "$#" -ne 1 ]; then printf $'Usage: %s \n\nFor instance `%s 2024-07`\n\n' "${0}" "${0}" exit 1 @@ -16,15 +16,12 @@ repository='leanprover-community/mathlib4' startDate="${1}" endDate="${2}" -# 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 -- note that there is a limit to how many commits `gh` returns commits_in_range="$(git log --since="${startDate}" --until="${endDate}" --pretty=oneline | wc -l)" -# Retrieve merged PRs from the given range +# Retrieve merged (i.e. closed, due to bors) 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)"' - # 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 @@ -35,7 +32,7 @@ git log --pretty=oneline --since="${startDate}" --until="${endDate}" | echo "$prs" } -# the current year and month +# the year and month being processed yr_mth="${1}" #"$(date +%Y-%m)" yr_mth_day=${yr_mth}-01 @@ -52,9 +49,6 @@ 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}" -#echo "First run: ${start_date} ${yr_mth}-15T23:59:59" -#echo "Second run: ${yr_mth}-16T00:00:00 ${end_date}" - ( findInRange "${start_date}" "${yr_mth}-15T23:59:59" | sed -z 's=]\n*$=,\n=' findInRange "${yr_mth}-16T00:00:00" "${end_date}" | sed -z 's=^\[==' From 0bf5e48366dae442486b9e0d52410c85eec1c654 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 16:28:49 +0200 Subject: [PATCH 53/65] better report --- monthly_summary.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/monthly_summary.sh b/monthly_summary.sh index 8b4570b8..9ae1d284 100755 --- a/monthly_summary.sh +++ b/monthly_summary.sh @@ -84,14 +84,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 (CI started in %s and ended 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` (CI started in %s and ended in %s?)\n%s\n' "${mth}" "${next_mth}" "${only_git}" fi printf -- $'---\n' From bf25e8149e1452836473e1f2c9f9cc29ed89a4b7 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 16:38:57 +0200 Subject: [PATCH 54/65] raw formatting --- .github/workflows/monthly_pr_report.yaml | 16 ++----------- monthly_summary.sh | 30 ++++++++++++++++++++---- 2 files changed, 28 insertions(+), 18 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 3b4d0ede..df69e098 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -35,18 +35,6 @@ jobs: mth="$(date -d "${yrMth}-01" '+%B')" title="### ${mth} in Mathlib summary" - mim="$(printf '%s\n\n%s\n' "${title}" "$(cd mathlib; ./../blog/monthly_summary.sh "${yrMth}")")" + mim="$(printf '%s\n\n%s\n' "${title}" "$(cd mathlib; ./../blog/monthly_summary.sh "${yrMth}" raw)")" echo "${mim}" - baseUrl="https://github.com/leanprover-community/mathlib4/pull/" - echo "${mim}" | - sed ' - / [0-9]* PRs$/{ - s=^=
\n= - s=$=\n\n= - } - s=^PR #\([0-9]*\)=* PR [#\1]('"${baseUrl}"'\1)=' | - sed -z ' - s=
=
= - s=\n---\nReports\n\n=\n
\n\n---\n\n
Reports\n\n= - s=\n---[\n]*$=\n\n
\n&= - ' > "${GITHUB_STEP_SUMMARY}" + printf '%s\n\n%s\n' "${title}" "$(cd mathlib; ./../blog/monthly_summary.sh "${yrMth}")" > "${GITHUB_STEP_SUMMARY}" diff --git a/monthly_summary.sh b/monthly_summary.sh index 9ae1d284..a6d86494 100755 --- a/monthly_summary.sh +++ b/monthly_summary.sh @@ -1,11 +1,18 @@ #!/bin/bash +{ # Check if required argument is provided -if [ "$#" -ne 1 ]; then - printf $'Usage: %s \n\nFor instance `%s 2024-07`\n\n' "${0}" "${0}" +if [ "$#" -gt 2 ]; then + printf $'Usages:\n%s \n%s raw\n\nFor instance `%s 2024-07`\n\nThe `raw` input skips .md formatting\n' "${0}" "${0}" "${0}" exit 1 fi +raw="" +if [ "${2}" == "raw" ] +then + raw=raw +fi + rm -rf found_by_gh.txt found_by_git.txt findInRange () { @@ -50,8 +57,8 @@ 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}" ( -findInRange "${start_date}" "${yr_mth}-15T23:59:59" | sed -z 's=]\n*$=,\n=' -findInRange "${yr_mth}-16T00:00:00" "${end_date}" | sed -z 's=^\[==' + findInRange "${start_date}" "${yr_mth}-15T23:59:59" | sed -z 's=]\n*$=,\n=' + findInRange "${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)"' | @@ -96,4 +103,19 @@ fi printf -- $'---\n' +baseUrl="https://github.com/${repository}/pull/" + rm -rf found_by_gh.txt found_by_git.txt +} | if [ -n "${raw}" ]; then cat; else # extra .md formatting + sed ' + / [0-9]* PRs$/{ + s=^=
\n= + s=$=\n\n= + } + s=^PR #\([0-9]*\)=* PR [#\1]('"${baseUrl}"'\1)=' | + sed -z ' + s=
=
= + s=\n---\nReports\n\n=\n
\n\n---\n\n
Reports\n\n= + s=\n---[\n]*$=\n\n
\n&= + ' +fi From 359ec80a08bf0c815c0f07337e8ebf17e9655dd9 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 16:41:42 +0200 Subject: [PATCH 55/65] url? --- .github/workflows/monthly_pr_report.yaml | 3 +-- monthly_summary.sh | 7 +++---- 2 files changed, 4 insertions(+), 6 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index df69e098..f146ee7e 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -35,6 +35,5 @@ jobs: mth="$(date -d "${yrMth}-01" '+%B')" title="### ${mth} in Mathlib summary" - mim="$(printf '%s\n\n%s\n' "${title}" "$(cd mathlib; ./../blog/monthly_summary.sh "${yrMth}" raw)")" - echo "${mim}" + printf '%s\n\n%s\n' "${title}" "$(cd mathlib; ./../blog/monthly_summary.sh "${yrMth}" raw)" printf '%s\n\n%s\n' "${title}" "$(cd mathlib; ./../blog/monthly_summary.sh "${yrMth}")" > "${GITHUB_STEP_SUMMARY}" diff --git a/monthly_summary.sh b/monthly_summary.sh index a6d86494..821ea88c 100755 --- a/monthly_summary.sh +++ b/monthly_summary.sh @@ -1,5 +1,8 @@ #!/bin/bash +repository='leanprover-community/mathlib4' +baseUrl="https://github.com/${repository}/pull/" + { # Check if required argument is provided if [ "$#" -gt 2 ]; then @@ -17,8 +20,6 @@ rm -rf found_by_gh.txt found_by_git.txt findInRange () { -repository='leanprover-community/mathlib4' - # Get the start and end dates startDate="${1}" endDate="${2}" @@ -103,8 +104,6 @@ fi printf -- $'---\n' -baseUrl="https://github.com/${repository}/pull/" - rm -rf found_by_gh.txt found_by_git.txt } | if [ -n "${raw}" ]; then cat; else # extra .md formatting sed ' From 7f66830b9db1db9c6b9ff2442d6efde574ca65fc Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 16:46:09 +0200 Subject: [PATCH 56/65] embed title --- .github/workflows/monthly_pr_report.yaml | 7 ++----- monthly_summary.sh | 13 +++++++++---- 2 files changed, 11 insertions(+), 9 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index f146ee7e..76b9eb01 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -32,8 +32,5 @@ jobs: - name: blog report run: | yrMth=2024-07 - mth="$(date -d "${yrMth}-01" '+%B')" - title="### ${mth} in Mathlib summary" - - printf '%s\n\n%s\n' "${title}" "$(cd mathlib; ./../blog/monthly_summary.sh "${yrMth}" raw)" - printf '%s\n\n%s\n' "${title}" "$(cd mathlib; ./../blog/monthly_summary.sh "${yrMth}")" > "${GITHUB_STEP_SUMMARY}" + printf '%s\n' "$(cd mathlib; ./../blog/monthly_summary.sh "${yrMth}" raw)" + printf '%s\n' "$(cd mathlib; ./../blog/monthly_summary.sh "${yrMth}")" > "${GITHUB_STEP_SUMMARY}" diff --git a/monthly_summary.sh b/monthly_summary.sh index 821ea88c..2605fbf6 100755 --- a/monthly_summary.sh +++ b/monthly_summary.sh @@ -3,6 +3,15 @@ repository='leanprover-community/mathlib4' baseUrl="https://github.com/${repository}/pull/" +# the year and month being processed +yr_mth="${1}" #"$(date +%Y-%m)" +yr_mth_day=${yr_mth}-01 + +mth="$(date -d "${yrMth}-01" '+%B')" +title="### ${mth} in Mathlib summary" + +printf '%s\n\n' "${title}" + { # Check if required argument is provided if [ "$#" -gt 2 ]; then @@ -40,10 +49,6 @@ git log --pretty=oneline --since="${startDate}" --until="${endDate}" | echo "$prs" } -# the year and month being processed -yr_mth="${1}" #"$(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 957c8fc261bb4ef9ff9fb827c8837880c3a7e043 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 16:49:01 +0200 Subject: [PATCH 57/65] shorten and correct date --- .github/workflows/monthly_pr_report.yaml | 5 +++-- monthly_summary.sh | 2 +- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml index 76b9eb01..d1d3df15 100644 --- a/.github/workflows/monthly_pr_report.yaml +++ b/.github/workflows/monthly_pr_report.yaml @@ -32,5 +32,6 @@ jobs: - name: blog report run: | yrMth=2024-07 - printf '%s\n' "$(cd mathlib; ./../blog/monthly_summary.sh "${yrMth}" raw)" - printf '%s\n' "$(cd mathlib; ./../blog/monthly_summary.sh "${yrMth}")" > "${GITHUB_STEP_SUMMARY}" + cd mathlib; + ./../blog/monthly_summary.sh "${yrMth}" raw + ./../blog/monthly_summary.sh "${yrMth}" > "${GITHUB_STEP_SUMMARY}" diff --git a/monthly_summary.sh b/monthly_summary.sh index 2605fbf6..64530fe7 100755 --- a/monthly_summary.sh +++ b/monthly_summary.sh @@ -7,7 +7,7 @@ baseUrl="https://github.com/${repository}/pull/" yr_mth="${1}" #"$(date +%Y-%m)" yr_mth_day=${yr_mth}-01 -mth="$(date -d "${yrMth}-01" '+%B')" +mth="$(date -d "${yr_mth_day}" '+%B')" title="### ${mth} in Mathlib summary" printf '%s\n\n' "${title}" From 44af846be2d0126b5c7964da7b511b350f4b2887 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 16:52:01 +0200 Subject: [PATCH 58/65] raw output with flag --- monthly_summary.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/monthly_summary.sh b/monthly_summary.sh index 64530fe7..69e69c90 100755 --- a/monthly_summary.sh +++ b/monthly_summary.sh @@ -110,7 +110,7 @@ fi printf -- $'---\n' rm -rf found_by_gh.txt found_by_git.txt -} | if [ -n "${raw}" ]; then cat; else # extra .md formatting +} | if [ "${raw}" == "raw" ]; then cat; else # extra .md formatting sed ' / [0-9]* PRs$/{ s=^=
\n= From 6e562ba5692b6f0805d2c374e36a3bfaa92bea36 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 16:55:54 +0200 Subject: [PATCH 59/65] simplify raw --- monthly_summary.sh | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/monthly_summary.sh b/monthly_summary.sh index 69e69c90..88e20fb9 100755 --- a/monthly_summary.sh +++ b/monthly_summary.sh @@ -1,5 +1,12 @@ #!/bin/bash +: <<'BASH_DOC_MODULE' + +This command + +BASH_DOC_MODULE + + repository='leanprover-community/mathlib4' baseUrl="https://github.com/${repository}/pull/" @@ -19,11 +26,7 @@ if [ "$#" -gt 2 ]; then exit 1 fi -raw="" -if [ "${2}" == "raw" ] -then - raw=raw -fi +raw="${2}" rm -rf found_by_gh.txt found_by_git.txt From dec36003db64ffa7ea48fb7afd5d0eb21d0eaa17 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 16:58:04 +0200 Subject: [PATCH 60/65] print raw --- monthly_summary.sh | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/monthly_summary.sh b/monthly_summary.sh index 88e20fb9..e470f664 100755 --- a/monthly_summary.sh +++ b/monthly_summary.sh @@ -2,7 +2,8 @@ : <<'BASH_DOC_MODULE' -This command +Running `monthly_summary.sh 2024-07` produces an md-formatted summary of all the PRs that were +merged into mathlib master in the month 2024-07 BASH_DOC_MODULE @@ -27,7 +28,7 @@ if [ "$#" -gt 2 ]; then fi raw="${2}" - +echo "raw is ${raw}" rm -rf found_by_gh.txt found_by_git.txt findInRange () { From dc8c7556979a5008d3e15c19499fca96d0df5aed Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 17:00:01 +0200 Subject: [PATCH 61/65] pipe conditionally --- monthly_summary.sh | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/monthly_summary.sh b/monthly_summary.sh index e470f664..a4870256 100755 --- a/monthly_summary.sh +++ b/monthly_summary.sh @@ -3,7 +3,10 @@ : <<'BASH_DOC_MODULE' Running `monthly_summary.sh 2024-07` produces an md-formatted summary of all the PRs that were -merged into mathlib master in the month 2024-07 +merged into mathlib master in the month 2024-07. +A "raw" format can be obtain running `monthly_summary.sh 2024-07 raw`. + +There is a slight discrepancy BASH_DOC_MODULE @@ -114,7 +117,7 @@ fi printf -- $'---\n' rm -rf found_by_gh.txt found_by_git.txt -} | if [ "${raw}" == "raw" ]; then cat; else # extra .md formatting +} | { if [ "${raw}" == "raw" ]; then cat; else # extra .md formatting sed ' / [0-9]* PRs$/{ s=^=
\n= @@ -126,4 +129,4 @@ rm -rf found_by_gh.txt found_by_git.txt s=\n---\nReports\n\n=\n
\n\n---\n\n
Reports\n\n= s=\n---[\n]*$=\n\n
\n&= ' -fi +fi } From d5afe927766f0645f578b643fb445680b300b631 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 17:10:21 +0200 Subject: [PATCH 62/65] semicolon --- monthly_summary.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/monthly_summary.sh b/monthly_summary.sh index a4870256..492f6244 100755 --- a/monthly_summary.sh +++ b/monthly_summary.sh @@ -129,4 +129,4 @@ rm -rf found_by_gh.txt found_by_git.txt s=\n---\nReports\n\n=\n\n\n---\n\n
Reports\n\n= s=\n---[\n]*$=\n\n
\n&= ' -fi } +fi ; } From ce1f2ef3ef62c5f5db4ba6c59085b8048fe00fef Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 17:12:51 +0200 Subject: [PATCH 63/65] spread out --- monthly_summary.sh | 31 ++++++++++++++++++------------- 1 file changed, 18 insertions(+), 13 deletions(-) diff --git a/monthly_summary.sh b/monthly_summary.sh index 492f6244..1c5cdfe2 100755 --- a/monthly_summary.sh +++ b/monthly_summary.sh @@ -117,16 +117,21 @@ fi printf -- $'---\n' rm -rf found_by_gh.txt found_by_git.txt -} | { if [ "${raw}" == "raw" ]; then cat; else # extra .md formatting - sed ' - / [0-9]* PRs$/{ - s=^=
\n= - s=$=\n\n= - } - s=^PR #\([0-9]*\)=* PR [#\1]('"${baseUrl}"'\1)=' | - sed -z ' - s=
=
= - s=\n---\nReports\n\n=\n
\n\n---\n\n
Reports\n\n= - s=\n---[\n]*$=\n\n
\n&= - ' -fi ; } +} | { + if [ "${raw}" == "raw" ] + then + cat - + else # extra .md formatting + sed ' + / [0-9]* PRs$/{ + s=^=
\n= + s=$=\n\n= + } + s=^PR #\([0-9]*\)=* PR [#\1]('"${baseUrl}"'\1)=' | + sed -z ' + s=
=
= + s=\n---\nReports\n\n=\n
\n\n---\n\n
Reports\n\n= + s=\n---[\n]*$=\n\n
\n&= + ' + fi + } From e19142b3c985125e250960af849bcd93327c8a99 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 17:16:43 +0200 Subject: [PATCH 64/65] gate --- monthly_summary.sh | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/monthly_summary.sh b/monthly_summary.sh index 1c5cdfe2..663a8905 100755 --- a/monthly_summary.sh +++ b/monthly_summary.sh @@ -30,8 +30,6 @@ if [ "$#" -gt 2 ]; then exit 1 fi -raw="${2}" -echo "raw is ${raw}" rm -rf found_by_gh.txt found_by_git.txt findInRange () { @@ -118,7 +116,7 @@ printf -- $'---\n' rm -rf found_by_gh.txt found_by_git.txt } | { - if [ "${raw}" == "raw" ] + if (( $2 == "raw" )) then cat - else # extra .md formatting From 91e3d1c65197df57eb04c7da7b49162e4bce0d6d Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 2 Aug 2024 17:52:10 +0200 Subject: [PATCH 65/65] docs --- monthly_summary.sh | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/monthly_summary.sh b/monthly_summary.sh index 663a8905..c9fb0fa3 100755 --- a/monthly_summary.sh +++ b/monthly_summary.sh @@ -4,13 +4,17 @@ Running `monthly_summary.sh 2024-07` produces an md-formatted summary of all the PRs that were merged into mathlib master in the month 2024-07. -A "raw" format can be obtain running `monthly_summary.sh 2024-07 raw`. +A "raw" format can be obtained running `monthly_summary.sh 2024-07 raw`. -There is a slight discrepancy +There is a slight discrepancy between the time when a PR is merged and when it passes CI. +The script looks at the time when CI was successful on the PR, not at the time when the +successful CI cycle started. +However, in the final `Reports` section, the script mentions the PRs at either end: +* the ones that starts CI in the previous month and finished it in the current month; +* the ones that starts CI in the current month and finished it in the following month. BASH_DOC_MODULE - repository='leanprover-community/mathlib4' baseUrl="https://github.com/${repository}/pull/"