diff --git a/.github/actionlint.yml b/.github/actionlint.yml new file mode 100644 index 0000000000..9135c9bb68 --- /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 0000000000..dd9a83c59a --- /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 diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 1e48fadc79..a728e5e9fd 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 }} diff --git a/.github/workflows/monthly_pr_report.yaml b/.github/workflows/monthly_pr_report.yaml new file mode 100644 index 0000000000..d1d3df1586 --- /dev/null +++ b/.github/workflows/monthly_pr_report.yaml @@ -0,0 +1,37 @@ +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 }} + + steps: + - name: cleanup + run: | + find . -name . -o -prune -exec rm -rf -- {} + + + - uses: actions/checkout@v4 + with: + path: blog + + - uses: actions/checkout@v4 + with: + repository: leanprover-community/mathlib4 + fetch-depth: 0 + ref: master + path: mathlib + + - name: blog report + run: | + yrMth=2024-07 + 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 new file mode 100755 index 0000000000..c9fb0fa396 --- /dev/null +++ b/monthly_summary.sh @@ -0,0 +1,139 @@ +#!/bin/bash + +: <<'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. +A "raw" format can be obtained running `monthly_summary.sh 2024-07 raw`. + +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/" + +# the year and month being processed +yr_mth="${1}" #"$(date +%Y-%m)" +yr_mth_day=${yr_mth}-01 + +mth="$(date -d "${yr_mth_day}" '+%B')" +title="### ${mth} in Mathlib summary" + +printf '%s\n\n' "${title}" + +{ +# Check if required argument is provided +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 + +rm -rf found_by_gh.txt found_by_git.txt + +findInRange () { + +# Get the start and end dates +startDate="${1}" +endDate="${2}" + +# 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 (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))") + +# 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" +} + +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 "${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)"' | + 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=^=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' + +if [ -z "${only_gh}" ] +then + printf $'* All PRs are accounted for!\n' +else + 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` (CI started in %s and ended in %s?)\n%s\n' "${mth}" "${next_mth}" "${only_git}" +fi + +printf -- $'---\n' + +rm -rf found_by_gh.txt found_by_git.txt +} | { + if (( $2 == "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 + }