From 082a85b0cf86f5cd9f5ef9871cc22b692fbc3be0 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 8 Jun 2022 11:08:25 +0100 Subject: [PATCH 01/11] Add a CI script to automate "this month in mathlib" --- .github/workflows/make-monthly-pr.yml | 43 +++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) create mode 100644 .github/workflows/make-monthly-pr.yml diff --git a/.github/workflows/make-monthly-pr.yml b/.github/workflows/make-monthly-pr.yml new file mode 100644 index 00000000..b20334ae --- /dev/null +++ b/.github/workflows/make-monthly-pr.yml @@ -0,0 +1,43 @@ +# This is a basic workflow to help you get started with Actions + +name: "Create 'This month in mathlib' PR" + +# Controls when the workflow will run +on: + # Allows you to run this workflow manually from the Actions tab + workflow_dispatch: + +# A workflow run is made up of one or more jobs that can run sequentially or in parallel +jobs: + # This workflow contains a single job called "build" + build: + # The type of runner that the job will run on + runs-on: ubuntu-latest + + # Steps represent a sequence of tasks that will be executed as part of the job + steps: + # Checks-out your repository under $GITHUB_WORKSPACE, so your job can access it + - uses: actions/checkout@v3 + with: + path: blog + - uses: actions/checkout@v3 + with: + repository: leanprover-community/mathlib + path: mathlib + + # Runs a single command using the runners shell + - name: Generate the blog post + id: generate + run: | + cd blog + # hack taken from https://www.gnu.org/software/coreutils/manual/html_node/Relative-items-in-date-strings.html + date="$(date +%Y-%m-15) -1 month" + date_info=$(date --date="$date" +"%Y %-m %m"); + echo "::set-output name=iso-date::$(date --date="$date" +"%Y-%m")" + ./monthly_blog "$(date --date="$date" +"%Y")" "$(date --date="$date" +"%-m")" ../mathlib + + - name: Create Pull Request + uses: peter-evans/create-pull-request@v4 + with: + branch: this-month-in-mathlib/${{ steps.generate.iso-date}} + title: This month in mathlib (${{ steps.generate.iso-date}}) From b887493b7a10adde3adacecb3e02e01b1fa4e687 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 8 Jun 2022 11:10:57 +0100 Subject: [PATCH 02/11] Update make-monthly-pr.yml --- .github/workflows/make-monthly-pr.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.github/workflows/make-monthly-pr.yml b/.github/workflows/make-monthly-pr.yml index b20334ae..6a6c5ed2 100644 --- a/.github/workflows/make-monthly-pr.yml +++ b/.github/workflows/make-monthly-pr.yml @@ -6,6 +6,9 @@ name: "Create 'This month in mathlib' PR" on: # Allows you to run this workflow manually from the Actions tab workflow_dispatch: + + push: + branches: [automate-this-month-in] # hack so that I can test this in the PR # A workflow run is made up of one or more jobs that can run sequentially or in parallel jobs: From d7e5dca03340df9750f99e0df9d61977c579a1e9 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 8 Jun 2022 11:11:40 +0100 Subject: [PATCH 03/11] Update make-monthly-pr.yml --- .github/workflows/make-monthly-pr.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/make-monthly-pr.yml b/.github/workflows/make-monthly-pr.yml index 6a6c5ed2..31322947 100644 --- a/.github/workflows/make-monthly-pr.yml +++ b/.github/workflows/make-monthly-pr.yml @@ -37,7 +37,7 @@ jobs: date="$(date +%Y-%m-15) -1 month" date_info=$(date --date="$date" +"%Y %-m %m"); echo "::set-output name=iso-date::$(date --date="$date" +"%Y-%m")" - ./monthly_blog "$(date --date="$date" +"%Y")" "$(date --date="$date" +"%-m")" ../mathlib + ./monthly_blog.sh "$(date --date="$date" +"%Y")" "$(date --date="$date" +"%-m")" ../mathlib - name: Create Pull Request uses: peter-evans/create-pull-request@v4 From aa276134b152e993b6ec48c2088880b78746dea1 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 8 Jun 2022 11:13:22 +0100 Subject: [PATCH 04/11] Update make-monthly-pr.yml --- .github/workflows/make-monthly-pr.yml | 15 +++------------ 1 file changed, 3 insertions(+), 12 deletions(-) diff --git a/.github/workflows/make-monthly-pr.yml b/.github/workflows/make-monthly-pr.yml index 31322947..7214254f 100644 --- a/.github/workflows/make-monthly-pr.yml +++ b/.github/workflows/make-monthly-pr.yml @@ -1,25 +1,17 @@ -# This is a basic workflow to help you get started with Actions - name: "Create 'This month in mathlib' PR" -# Controls when the workflow will run on: - # Allows you to run this workflow manually from the Actions tab + # Allows us to run this workflow manually from the Actions tab workflow_dispatch: push: branches: [automate-this-month-in] # hack so that I can test this in the PR -# A workflow run is made up of one or more jobs that can run sequentially or in parallel jobs: - # This workflow contains a single job called "build" - build: - # The type of runner that the job will run on + generate: runs-on: ubuntu-latest - # Steps represent a sequence of tasks that will be executed as part of the job steps: - # Checks-out your repository under $GITHUB_WORKSPACE, so your job can access it - uses: actions/checkout@v3 with: path: blog @@ -28,7 +20,6 @@ jobs: repository: leanprover-community/mathlib path: mathlib - # Runs a single command using the runners shell - name: Generate the blog post id: generate run: | @@ -37,7 +28,7 @@ jobs: date="$(date +%Y-%m-15) -1 month" date_info=$(date --date="$date" +"%Y %-m %m"); echo "::set-output name=iso-date::$(date --date="$date" +"%Y-%m")" - ./monthly_blog.sh "$(date --date="$date" +"%Y")" "$(date --date="$date" +"%-m")" ../mathlib + ./monthly-blog.sh "$(date --date="$date" +"%Y")" "$(date --date="$date" +"%-m")" ../mathlib - name: Create Pull Request uses: peter-evans/create-pull-request@v4 From 201c27df581bb5b0b420d1f7c142d9a171469ead Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 8 Jun 2022 11:14:15 +0100 Subject: [PATCH 05/11] Update make-monthly-pr.yml --- .github/workflows/make-monthly-pr.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/make-monthly-pr.yml b/.github/workflows/make-monthly-pr.yml index 7214254f..268307d2 100644 --- a/.github/workflows/make-monthly-pr.yml +++ b/.github/workflows/make-monthly-pr.yml @@ -35,3 +35,4 @@ jobs: with: branch: this-month-in-mathlib/${{ steps.generate.iso-date}} title: This month in mathlib (${{ steps.generate.iso-date}}) + path: blog From 43710bc3ee3b226a15dc56623f752e5dcc81d7a8 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 8 Jun 2022 11:20:00 +0100 Subject: [PATCH 06/11] Update make-monthly-pr.yml --- .github/workflows/make-monthly-pr.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/make-monthly-pr.yml b/.github/workflows/make-monthly-pr.yml index 268307d2..0e884f11 100644 --- a/.github/workflows/make-monthly-pr.yml +++ b/.github/workflows/make-monthly-pr.yml @@ -28,11 +28,11 @@ jobs: date="$(date +%Y-%m-15) -1 month" date_info=$(date --date="$date" +"%Y %-m %m"); echo "::set-output name=iso-date::$(date --date="$date" +"%Y-%m")" - ./monthly-blog.sh "$(date --date="$date" +"%Y")" "$(date --date="$date" +"%-m")" ../mathlib + ./monthly-blog.sh "$(date --date="$date" +"%Y")" "$(date --date="$date" +"%-m")" ../mathlib > posts/month-in-mathlib-${$(date --date="$date" +"%b-%Y"),,}.md - name: Create Pull Request uses: peter-evans/create-pull-request@v4 with: - branch: this-month-in-mathlib/${{ steps.generate.iso-date}} - title: This month in mathlib (${{ steps.generate.iso-date}}) + branch: this-month-in-mathlib/${{ steps.generate.outputs.iso-date }} + title: This month in mathlib (${{ steps.generate.outputs.iso-date }}) path: blog From b17667ee6ebd9923088afb08f7e06f45bb7a312c Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 8 Jun 2022 11:23:51 +0100 Subject: [PATCH 07/11] Tidy --- .github/workflows/make-monthly-pr.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/make-monthly-pr.yml b/.github/workflows/make-monthly-pr.yml index 0e884f11..7abde002 100644 --- a/.github/workflows/make-monthly-pr.yml +++ b/.github/workflows/make-monthly-pr.yml @@ -24,9 +24,9 @@ jobs: id: generate run: | cd blog - # hack taken from https://www.gnu.org/software/coreutils/manual/html_node/Relative-items-in-date-strings.html + # get the first day of last month. Hack taken from https://www.gnu.org/software/coreutils/manual/html_node/Relative-items-in-date-strings.html date="$(date +%Y-%m-15) -1 month" - date_info=$(date --date="$date" +"%Y %-m %m"); + date="$(date --date "$date" +%Y-%m-01)" echo "::set-output name=iso-date::$(date --date="$date" +"%Y-%m")" ./monthly-blog.sh "$(date --date="$date" +"%Y")" "$(date --date="$date" +"%-m")" ../mathlib > posts/month-in-mathlib-${$(date --date="$date" +"%b-%Y"),,}.md From 0c1077c968b33b693d256d2de2fc06c213e16b2e Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 8 Jun 2022 11:25:34 +0100 Subject: [PATCH 08/11] Update make-monthly-pr.yml --- .github/workflows/make-monthly-pr.yml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/.github/workflows/make-monthly-pr.yml b/.github/workflows/make-monthly-pr.yml index 7abde002..d8627dcf 100644 --- a/.github/workflows/make-monthly-pr.yml +++ b/.github/workflows/make-monthly-pr.yml @@ -28,7 +28,9 @@ jobs: date="$(date +%Y-%m-15) -1 month" date="$(date --date "$date" +%Y-%m-01)" echo "::set-output name=iso-date::$(date --date="$date" +"%Y-%m")" - ./monthly-blog.sh "$(date --date="$date" +"%Y")" "$(date --date="$date" +"%-m")" ../mathlib > posts/month-in-mathlib-${$(date --date="$date" +"%b-%Y"),,}.md + slug_date="$(date --date="$date" +"%b-%Y")"; + slug_date="${slug_date,,}"; # lowercase + ./monthly-blog.sh "$(date --date="$date" +"%Y")" "$(date --date="$date" +"%-m")" ../mathlib > posts/month-in-mathlib-$slug_date.md - name: Create Pull Request uses: peter-evans/create-pull-request@v4 From 17cc19df1c3be842f1917a51fc0a3e87a4b3898d Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 8 Jun 2022 11:29:45 +0100 Subject: [PATCH 09/11] Update make-monthly-pr.yml --- .github/workflows/make-monthly-pr.yml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/.github/workflows/make-monthly-pr.yml b/.github/workflows/make-monthly-pr.yml index d8627dcf..191346d7 100644 --- a/.github/workflows/make-monthly-pr.yml +++ b/.github/workflows/make-monthly-pr.yml @@ -23,13 +23,18 @@ jobs: - name: Generate the blog post id: generate run: | - cd blog # get the first day of last month. Hack taken from https://www.gnu.org/software/coreutils/manual/html_node/Relative-items-in-date-strings.html date="$(date +%Y-%m-15) -1 month" date="$(date --date "$date" +%Y-%m-01)" echo "::set-output name=iso-date::$(date --date="$date" +"%Y-%m")" slug_date="$(date --date="$date" +"%b-%Y")"; slug_date="${slug_date,,}"; # lowercase + + # fetch all the commits from that date onwards + ( cd mathlib; + git fetch origin master --shallow-since="$date" ); + + cd blog ./monthly-blog.sh "$(date --date="$date" +"%Y")" "$(date --date="$date" +"%-m")" ../mathlib > posts/month-in-mathlib-$slug_date.md - name: Create Pull Request From ae7ce344869b2d9c3bb6f963ecfb9c798e826a08 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 8 Jun 2022 11:34:59 +0100 Subject: [PATCH 10/11] Update make-monthly-pr.yml --- .github/workflows/make-monthly-pr.yml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/.github/workflows/make-monthly-pr.yml b/.github/workflows/make-monthly-pr.yml index 191346d7..dd6a1e72 100644 --- a/.github/workflows/make-monthly-pr.yml +++ b/.github/workflows/make-monthly-pr.yml @@ -42,4 +42,8 @@ jobs: with: branch: this-month-in-mathlib/${{ steps.generate.outputs.iso-date }} title: This month in mathlib (${{ steps.generate.outputs.iso-date }}) + commit-message: Auto-generated PR log for ${{ steps.generate.outputs.iso-date }} + body: | + This pull request was generated by a manual trigger of the [`make-monthly-pr`](https://github.com/leanprover-community/blog/actions/workflows/make-monthly-pr.yml) + action in this repository. path: blog From b20c6f5553433b4811c8567cb7eb83fe27dc841b Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 8 Jun 2022 11:37:43 +0100 Subject: [PATCH 11/11] Finalize --- .github/workflows/make-monthly-pr.yml | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/.github/workflows/make-monthly-pr.yml b/.github/workflows/make-monthly-pr.yml index dd6a1e72..c4716862 100644 --- a/.github/workflows/make-monthly-pr.yml +++ b/.github/workflows/make-monthly-pr.yml @@ -1,11 +1,9 @@ name: "Create 'This month in mathlib' PR" +# This workflow will overwrite any currently open PR for the previous month. Do not run it once a maintainer has started curating the month! on: # Allows us to run this workflow manually from the Actions tab workflow_dispatch: - - push: - branches: [automate-this-month-in] # hack so that I can test this in the PR jobs: generate: @@ -44,6 +42,5 @@ jobs: title: This month in mathlib (${{ steps.generate.outputs.iso-date }}) commit-message: Auto-generated PR log for ${{ steps.generate.outputs.iso-date }} body: | - This pull request was generated by a manual trigger of the [`make-monthly-pr`](https://github.com/leanprover-community/blog/actions/workflows/make-monthly-pr.yml) - action in this repository. + This pull request was generated by a manual trigger of the [`make-monthly-pr`](https://github.com/leanprover-community/blog/actions/workflows/make-monthly-pr.yml) action in this repository. path: blog