pr-deploy.yml

name: "Deploy PR for review"

on:
    workflow_run: # https://docs.github.com/en/actions/using-workflows/events-that-trigger-workflows#workflow_run
        workflows: [Build and check HTML]
        types: [completed]

permissions:
    pull-requests: write

jobs:
    deploy:
        if:
            github.event.workflow_run.conclusion == 'success' && github.event.workflow_run.event ==
            'pull_request' && github.repository == 'leanprover/reference-manual'
        runs-on: ubuntu-latest
        steps:
            - name: Retrieve information about the original workflow
              uses: potiuk/get-workflow-origin@v1_1 # https://github.com/marketplace/actions/get-workflow-origin
              # This action is deprecated and archived, but it seems hard to find a
              # better solution for getting the PR number
              # see https://github.com/orgs/community/discussions/25220 for some discussion
              id: workflow-info
              with:
                  token: ${{ secrets.GITHUB_TOKEN }}
                  sourceRunId: ${{ github.event.workflow_run.id }}

            - name: Download artifact
              if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
              id: download-artifact
              uses: dawidd6/action-download-artifact@v7
              with:
                  run_id: ${{ github.event.workflow_run.id }}
                  name: "html"
                  path: _out
                  allow_forks: true

            # Detect whether we have the new combined site structure or the old single-site structure
            - name: Detect deployment structure
              id: detect-structure
              run: |
                  # Individual redirects are more readable than grouped output for simple variable assignments
                  # shellcheck disable=SC2129
                  if [ -d "_out/site" ]; then
                    echo "structure=new" >> "$GITHUB_OUTPUT"
                    echo "site_dir=_out/site" >> "$GITHUB_OUTPUT"
                    echo "draft_dir=_out/draft-site" >> "$GITHUB_OUTPUT"
                  else
                    echo "structure=old" >> "$GITHUB_OUTPUT"
                    echo "site_dir=_out/html-multi" >> "$GITHUB_OUTPUT"
                    echo "draft_dir=_out/draft/html-multi" >> "$GITHUB_OUTPUT"
                  fi

            # deploy-alias computes a URL component for the PR preview. This
            # is so we can have a stable name to use for feedback on draft
            # material.
            - id: deploy-alias
              uses: actions/github-script@v7
              name: Compute Alias
              if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
              with:
                  result-encoding: string
                  script: |
                      if (process.env.PR) {
                          return `pr-${process.env.PR}`
                      } else {
                          return 'deploy-preview-main';
                      }
              env:
                  PR: ${{ steps.workflow-info.outputs.pullRequestNumber }}

            - name: Deploy current draft
              id: deploy-draft
              if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
              uses: nwtgck/actions-netlify@v2.0
              with:
                  publish-dir: ${{ steps.detect-structure.outputs.site_dir }}
                  production-deploy: false
                  github-token: ${{ secrets.GITHUB_TOKEN }}
                  deploy-message: |
                      ${{ format('pr#{0}', steps.workflow-info.outputs.pullRequestNumber) }}
                  alias: ${{ steps.deploy-alias.outputs.result }}
                  enable-commit-comment: false
                  enable-pull-request-comment: false
                  github-deployment-environment: |
                      ${{ format('lean-ref-pr-#{0}', steps.workflow-info.outputs.pullRequestNumber) || 'lean-ref' }}
                  github-deployment-description: |
                      Draft without proofreading info
                  fails-without-credentials: true
              env:
                  NETLIFY_AUTH_TOKEN: ${{ secrets.NETLIFY_AUTH_TOKEN }}
                  NETLIFY_SITE_ID: "32e0f63e-7a18-4bf9-87f4-713650c7db70"

            # When pushing to `main` or a PR branch, deploy it with proofreading info as well
            - name: Deploy with proofreading info (draft mode, for PRs)
              id: deploy-draft-proofreading
              uses: nwtgck/actions-netlify@v2.0
              if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
              with:
                  publish-dir: ${{ steps.detect-structure.outputs.draft_dir }}
                  production-deploy: false
                  github-token: ${{ secrets.GITHUB_TOKEN }}
                  deploy-message: |
                      ${{ format('pr#{0} proofreading', steps.workflow-info.outputs.pullRequestNumber) }}
                  alias: draft-${{ steps.deploy-alias.outputs.result }}
                  enable-commit-comment: false
                  enable-pull-request-comment: false
                  github-deployment-environment: |
                      ${{ format('lean-ref-pr-draft-#{0}', steps.workflow-info.outputs.pullRequestNumber) }}
                  github-deployment-description: |
                      Draft with proofreading info
                  fails-without-credentials: true
              env:
                  NETLIFY_AUTH_TOKEN: ${{ secrets.NETLIFY_AUTH_TOKEN }}
                  NETLIFY_SITE_ID: "32e0f63e-7a18-4bf9-87f4-713650c7db70"

            # actions-netlify cannot add deploy links to a PR because it assumes a
            # pull_request context, not a workflow_run context, see
            # https://github.com/nwtgck/actions-netlify/issues/545
            # We work around by using a comment to post the latest link
            - name: "Comment on PR with preview links"
              uses: marocchino/sticky-pull-request-comment@v2
              with:
                  number: ${{ env.PR_NUMBER }}
                  header: preview-comment
                  recreate: true
                  message: |
                      [Preview for this PR](${{ steps.deploy-draft.outputs.deploy-url }}) is ready! :tada: [(also as a proofreading version)](${{ steps.deploy-draft-proofreading.outputs.deploy-url }}). built with commit ${{ env.PR_HEADSHA }}.
              env:
                  PR_NUMBER: ${{ steps.workflow-info.outputs.pullRequestNumber }}
                  PR_HEADSHA: ${{ steps.workflow-info.outputs.sourceHeadSha }}