diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml new file mode 100644 index 00000000000000..640d16934c6847 --- /dev/null +++ b/.github/workflows/monthly_pr_report.yaml @@ -0,0 +1,49 @@ +on: + pull_request + #schedule: + #- cron: '0 0 1 * *' # Runs at 00:00 on day 1 of the month + #workflow_dispatch: + +name: Blog report + +jobs: + + Monthly_PRs: + if: github.repository == 'leanprover-community/mathlib4' && github.event.pull_request.draft == false + name: Blog draft + runs-on: ubuntu-latest + + env: + GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} + BRANCH_NAME: ${{ github.head_ref }} + + steps: + - name: cleanup + run: | + find . -name . -o -prune -exec rm -rf -- {} + + + - uses: actions/checkout@v4 + with: + repository: leanprover-community/mathlib4 + fetch-depth: 0 + ref: master + + - 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')" + 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} ${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 + 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}" | tee "${tmp_file}" + + ./scripts/update_PR_comment.sh "${tmp_file}" "${title}" "${PR}" 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 diff --git a/scripts/find_labels.sh b/scripts/find_labels.sh new file mode 100755 index 00000000000000..5f56c8df13bc95 --- /dev/null +++ b/scripts/find_labels.sh @@ -0,0 +1,140 @@ +#!/bin/bash + : << 'BASH_MODULE_DOCS' + +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. + +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 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 + +forZulip=true +repository="${1}" + +# Get the start and end dates +startDate="${2}" +endDate="${3}" + +# 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 +prs=$(gh pr list --repo "$repository" --state closed --base master --search "closed:${startDate}..${endDate}" --json number,labels,title,author --limit "$((commits_in_range * 2))") + +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)"' | + 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]]) + } + } + ')" + +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= + ' +} + +# 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 '()' +)" + +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 +)" + +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}" + printf $'\n```spoiler Reports\n\n%s\n' "${reports}" + printf -- $'```\n' +else + formatForGitHub "${formattedPRs}" + printf $'
\n\n
Reports\n\n%s\n' "${reports}" + printf $'
\n' +fi