pr-deploy.yml

name: Deploy PR Preview

on:
    workflow_run:
        workflows: ["Continuous Integration"]
        types:
            - completed

permissions:
    actions: read
    contents: read
    deployments: write
    issues: write
    pull-requests: read

jobs:
    deploy:
        name: Deploy PR preview to Netlify
        runs-on: ubuntu-latest
        # Only run when:
        # - The triggering workflow succeeded
        # - The triggering event was a pull_request
        # - We're in the official repository (not a fork)
        if: >
            github.event.workflow_run.conclusion == 'success' && github.event.workflow_run.event ==
            'pull_request' && github.repository == 'leanprover/verso'
        steps:
            # This workflow can use repository secrets, so it runs after PR CI
            # instead of directly on pull_request. It deploys the CI artifact
            # without checking out or executing pull-request code.
            - name: Resolve PR information
              uses: actions/github-script@v9
              id: pr-info
              with:
                  script: |
                      const run = context.payload.workflow_run;
                      if (!run) {
                        core.setFailed('No triggering workflow_run payload was available.');
                        return;
                      }

                      const headRepo = run.head_repository?.full_name;
                      const headOwner =
                        run.head_repository?.owner?.login ?? headRepo?.split('/')[0];
                      const headBranch = run.head_branch;
                      const sourceHeadSha = run.head_sha;

                      if (!(headRepo && headOwner && headBranch && sourceHeadSha)) {
                        core.setFailed(
                          'The triggering workflow run did not include complete PR head metadata.'
                        );
                        return;
                      }

                      const {data: pulls} = await github.rest.pulls.list({
                        owner: context.repo.owner,
                        repo: context.repo.repo,
                        state: 'open',
                        head: `${headOwner}:${headBranch}`,
                        per_page: 10
                      });

                      const matches = pulls.filter(
                        (pull) =>
                          pull.head.sha === sourceHeadSha &&
                          pull.head.ref === headBranch &&
                          pull.head.repo?.full_name === headRepo &&
                          pull.base.repo?.full_name ===
                            `${context.repo.owner}/${context.repo.repo}`
                      );

                      if (matches.length !== 1) {
                        core.setFailed(
                          `Expected exactly one open PR for ${headRepo}:${headBranch} at ${sourceHeadSha}, got ${matches.length}.`
                        );
                        return;
                      }

                      const pull = matches[0];
                      core.setOutput('pullRequestNumber', String(pull.number));
                      core.setOutput('pullRequestTitle', pull.title);
                      core.setOutput('sourceHeadSha', sourceHeadSha);
                      core.setOutput('targetCommitSha', pull.merge_commit_sha || '');
                      core.info(
                        `Resolved PR #${pull.number}: source ${sourceHeadSha}, target ${pull.merge_commit_sha || '<missing>'}`
                      );

            - name: Validate PR metadata
              env:
                  PULL_REQUEST_NUMBER: ${{ steps.pr-info.outputs.pullRequestNumber }}
                  SOURCE_HEAD_SHA: ${{ steps.pr-info.outputs.sourceHeadSha }}
                  TARGET_COMMIT_SHA: ${{ steps.pr-info.outputs.targetCommitSha }}
              run: |
                  if [ -z "$PULL_REQUEST_NUMBER" ]; then
                      echo "::error::No pull request number was available for the deployment."
                      exit 1
                  fi
                  if [ -z "$SOURCE_HEAD_SHA" ] && [ -z "$TARGET_COMMIT_SHA" ]; then
                      echo "::error::No PR commit SHA was available for the deployment."
                      exit 1
                  fi

            - name: Download HTML manual artifact
              uses: actions/download-artifact@v8
              with:
                  run-id: ${{ github.event.workflow_run.id }}
                  github-token: ${{ secrets.GITHUB_TOKEN }}
                  name: html-manual-for-deploy
                  path: html-manual

            # This third-party action is pinned because it receives the Netlify
            # token. GitHub reporting is disabled here and handled below.
            - name: Deploy to Netlify
              id: netlify
              uses: nwtgck/actions-netlify@d22a32a27c918fe470bbc562e984f80ec48c2668
              with:
                  publish-dir: html-manual
                  production-deploy: false
                  alias: verso-pr-${{ steps.pr-info.outputs.pullRequestNumber }}
                  deploy-message:
                      "pr#${{ steps.pr-info.outputs.pullRequestNumber }}: ${{
                      steps.pr-info.outputs.pullRequestTitle }}"
                  enable-commit-comment: false
                  enable-pull-request-comment: false
                  # Under workflow_run, actions-netlify falls back to the
                  # default-branch context.sha for GitHub reporting. It has no
                  # deployment ref/SHA override, so record the deployment below.
                  enable-commit-status: false
                  enable-github-deployment: false
                  fails-without-credentials: true
              env:
                  NETLIFY_AUTH_TOKEN: ${{ secrets.NETLIFY_AUTH_TOKEN }}
                  NETLIFY_SITE_ID: "8a89abd8-095b-4496-a9c1-381d2d5629ec"

            # The deployment should point at the PR test/merge SHA when
            # available, not the default-branch SHA of this workflow_run job.
            - name: Record GitHub deployment
              uses: actions/github-script@v9
              env:
                  DEPLOY_ENVIRONMENT: "verso-pr-#${{ steps.pr-info.outputs.pullRequestNumber }}"
                  DEPLOY_SOURCE_SHA: ${{ steps.pr-info.outputs.sourceHeadSha }}
                  DEPLOY_TARGET_SHA: ${{ steps.pr-info.outputs.targetCommitSha }}
                  DEPLOY_URL: ${{ steps.netlify.outputs.deploy-url }}
              with:
                  script: |
                      const owner = context.repo.owner;
                      const repo = context.repo.repo;
                      const environment = process.env.DEPLOY_ENVIRONMENT;
                      const deployUrl = process.env.DEPLOY_URL;
                      const sourceSha = process.env.DEPLOY_SOURCE_SHA;
                      const targetSha = process.env.DEPLOY_TARGET_SHA;
                      const ref = targetSha || sourceSha;
                      const logUrl = context.payload.workflow_run?.html_url;

                      core.info(`PR deployment source SHA: ${sourceSha || '<missing>'}`);
                      core.info(`PR deployment target SHA: ${targetSha || '<missing>'}`);

                      if (!ref) {
                        core.setFailed('No PR commit SHA was available for the deployment.');
                        return;
                      }
                      if (!deployUrl) {
                        core.setFailed('Netlify did not report a deploy URL.');
                        return;
                      }

                      const deployment = await github.rest.repos.createDeployment({
                        owner,
                        repo,
                        ref,
                        task: 'deploy',
                        auto_merge: false,
                        required_contexts: [],
                        environment,
                        description: `Verso manual preview for ${environment}`,
                        transient_environment: true,
                        production_environment: false,
                      });

                      await github.rest.repos.createDeploymentStatus({
                        owner,
                        repo,
                        deployment_id: deployment.data.id,
                        state: 'success',
                        environment,
                        environment_url: deployUrl,
                        log_url: logUrl,
                        description: 'Netlify preview is ready',
                        auto_inactive: true,
                      });

                      core.info(
                        `Recorded ${environment} deployment ${deployment.data.id} for ${ref}: ${deployUrl}`
                      );

            # Keep the existing PR-comment signal while the deployment-based
            # preview path is validated.
            - name: Post deployment comment on PR
              uses: actions/github-script@v9
              env:
                  DEPLOY_URL: ${{ steps.netlify.outputs.deploy-url }}
                  PULL_REQUEST_NUMBER: ${{ steps.pr-info.outputs.pullRequestNumber }}
              with:
                  script: |
                      const deployUrl = process.env.DEPLOY_URL;
                      const pullNumber = Number(process.env.PULL_REQUEST_NUMBER);

                      if (!deployUrl) {
                        core.setFailed('Netlify did not report a deploy URL.');
                        return;
                      }
                      if (!Number.isInteger(pullNumber) || pullNumber <= 0) {
                        core.setFailed('No pull request number was available for the comment.');
                        return;
                      }

                      await github.rest.issues.createComment({
                        owner: context.repo.owner,
                        repo: context.repo.repo,
                        issue_number: pullNumber,
                        body: `[Preview for this PR](${deployUrl}) is ready! :tada:`
                      });