ml_stats_label.yaml

name: Add comment
on:
  pull_request:
    types:
      - labeled
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 #actions/checkout@v4
        #with:
        #  ## fetch the whole repository, to get the history of the last week
        #  fetch-depth: 0
        #  ref: 'master'

        #- uses: actions/checkout@v4
        #  with:
        #    ## fetch the whole repository, to get the history of the last week
        #    fetch-depth: 0
        #    ref: 'master'

      - 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 }}