Skip to content

add script and action for monthly PR summary #22

add script and action for monthly PR summary

add script and action for monthly PR summary #22

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/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
- uses: actions/checkout@v4
with:
repository: leanprover-community/mathlib4
#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
#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}" |
sed '
/ [0-9]* PRs$/{
s=^=</details><details><summary>\n=
s=$=\n</summary>\n=
}
s=^PR #\([0-9]*\)=* PR [#\1]('"${baseUrl}"'\1)=' |
sed -z '
s=</details><details><summary>=<details><summary>=
s=\n---\nReports\n\n=\n</details>\n\n---\n\n<details><summary>Reports</summary>\n\n=
s=\n---[\n]*$=\n\n</details>\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}"
# 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"
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"