feat: Mathlib weekly reports #1
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # This workflow is triggered by the label `test-ci`. It is meant to be useful to debug | |
| # the PR, since I think that the cron job cannot run on a PR. | |
| name: Add comment on PR and post to Zulip | |
| on: | |
| pull_request: | |
| types: | |
| - labeled | |
| schedule: | |
| - cron: "*/5 * * * *" | |
| jobs: | |
| add-comment: | |
| if: github.event.label.name == 'test-ci' | |
| runs-on: ubuntu-latest | |
| permissions: | |
| pull-requests: write | |
| steps: | |
| - name: Checkout master branch | |
| uses: adomani/get_mathlib4_with_cache@v1 | |
| - id: mathlib_stats | |
| run: | | |
| git checkout origin/adomani/periodic_reports_dev_custom_action scripts/mathlib_stats.sh scripts/count_decls.lean | |
| printf $'summary<<EOF\n%s\nEOF' "$(./scripts/mathlib_stats.sh)" >> "$GITHUB_OUTPUT" | |
| printf '%s\n' "$(./scripts/mathlib_stats.sh)" | |
| - name: Add comment | |
| run: gh pr comment "$NUMBER" --body "$BODY" | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| GH_REPO: ${{ github.repository }} | |
| NUMBER: ${{ github.event.pull_request.number }} | |
| BODY: ${{ steps.mathlib_stats.outputs.summary }} | |
| - name: Post report on Zulip | |
| uses: zulip/github-actions-zulip/send-message@v1 | |
| with: | |
| api-key: ${{ secrets.ZULIP_API_KEY }} | |
| email: '[email protected]' | |
| organization-url: 'https://leanprover.zulipchat.com' | |
| to: 'mathlib4' | |
| type: 'stream' | |
| topic: 'Mathlib weekly change report' | |
| content: ${{ steps.mathlib_stats.outputs.summary }} |