build-pr.yml

name: build test site on trigger comment

on:
  issue_comment:
    types: [created]

jobs:
  deploy:
    name: Deploy
    runs-on: doc-gen
    if: (toJSON(github.event.issue.pull_request) != 'null') && (startsWith(github.event.comment.body, '#deploy') || contains(toJSON(github.event.comment.body), '\r\n#deploy'))
    steps:
      - uses: octokit/request-action@v2.x
        name: Get PR head
        id: get_pr_head
        with:
          route: GET /repos/:repository/pulls/:pull_number
          repository: ${{ github.repository }}
          pull_number: ${{ github.event.issue.number }}
        env:
          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

      # Parse steps.get_pr_head.outputs.data, since it is a string
      - id: parse_pr_head
        name: Parse PR head
        uses: gr2m/get-json-paths-action@v1.x
        with:
          json: ${{ steps.get_pr_head.outputs.data }}
          head_user: 'head.user.login'

      - uses: octokit/request-action@v2.x
        name: Get comment author
        id: get_user
        with:
          route: GET /repos/:repository/collaborators/:username/permission
          repository: ${{ github.repository }}
          username: ${{ github.event.comment.user.login }}
        env:
          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

      # Parse steps.get_user.outputs.data, since it is a string
      - id: parse_user
        name: Parse comment author permission
        uses: gr2m/get-json-paths-action@v1.x
        with:
          json: ${{ steps.get_user.outputs.data }}
          permission: 'permission'

      - name: Add reaction
        if: (steps.parse_user.outputs.permission == 'admin')
        uses: peter-evans/create-or-update-comment@v1
        with:
          comment-id: ${{ github.event.comment.id }}
          reactions: rocket

      # this step is needed to get the PR ref from an issue comment
      # https://github.com/actions/checkout/issues/331
      - uses: actions/github-script@v3
        if: (steps.parse_user.outputs.permission == 'admin')
        id: get-pr
        with:
          script: |
            const request = {
              owner: context.repo.owner,
              repo: context.repo.repo,
              pull_number: context.issue.number
            }
            core.info(`Getting PR #${request.pull_number} from ${request.owner}/${request.repo}`)
            try {
              const result = await github.pulls.get(request)
              return result.data
            } catch (err) {
              core.setFailed(`Request failed with error ${err}`)
            }
      - uses: actions/checkout@v2
        if: (steps.parse_user.outputs.permission == 'admin')
        with:
          repository: ${{ fromJSON(steps.get-pr.outputs.result).head.repo.full_name }}
          ref: ${{ fromJSON(steps.get-pr.outputs.result).head.sha }} # or .head.ref for branch name

      - name: Checkout mathlib
        if: (steps.parse_user.outputs.permission == 'admin')
        run: git clone https://github.com/leanprover-community/mathlib

      - name: install elan
        if: (steps.parse_user.outputs.permission == 'admin')
        run: |
          set -o pipefail
          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
          cd mathlib
          ~/.elan/bin/lean --version
          echo "$HOME/.elan/bin" >> $GITHUB_PATH

      # - name: install Python
      #   if: (steps.parse_user.outputs.permission == 'admin')
      #   uses: actions/setup-python@v1
      #   with:
      #     python-version: 3.8

      - name: setup python venv
        if: (steps.parse_user.outputs.permission == 'admin')
        run: |
          python3 -m venv .venv
          echo "$PWD/.venv/bin" >> $GITHUB_PATH

      - name: install Python dependencies
        if: (steps.parse_user.outputs.permission == 'admin')
        run: |
          python -m pip install --upgrade pip
          pip install -r requirements.txt

      - name: run leanproject
        if: (steps.parse_user.outputs.permission == 'admin')
        run: |
          cd mathlib
          leanproject up

      - name: generate docs
        if: (steps.parse_user.outputs.permission == 'admin')
        run: ./deploy_docs.sh "mathlib" ".." "mathlib" "leanprover-community" "mathlib_docs_demo" "true"
        env:
          DEPLOY_GITHUB_TOKEN: ${{ secrets.DEPLOY_GITHUB_TOKEN }}
          github_repo: ${{ github.repository }}
          github_event: ${{ github.event_name }}
          github_ref: ${{ github.ref }}

      # https://stackoverflow.com/questions/58066966/commenting-a-pull-request-in-a-github-action
      - name: Post link
        if: (steps.parse_user.outputs.permission == 'admin')
        env:
          URL: ${{ github.event.issue.comments_url }}
          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
        run: |
          curl \
            -X POST \
            $URL \
            -H "Content-Type: application/json" \
            -H "Authorization: token $GITHUB_TOKEN" \
            --data '{ "body": "This PR has been successfully deployed! You can find it at <http://leanprover-community.github.io/mathlib_docs_demo> in around 10 minutes, or watch the deployment progress by going to <http://github.com/leanprover-community/mathlib_docs_demo>" }'

      - name: clean up working directory and elan
        if: always()
        run: rm -rf * $HOME/.elan