ci.yml

on:
  push:
    branches:
      - main
  pull_request:
    branches:
      - main
  release:
    types:
      - published
      - released

name: Build and deploy sites

jobs:
  build:
    name: Build site and generate HTML
    runs-on: ubuntu-latest
    outputs:
      ref-url: ${{ steps.deploy.outputs.deploy-url }}

    steps:
      - name: Install deps for figures (OS packages)
        run: |
          sudo apt update && sudo apt install -y poppler-utils

      - name: Install deps for figures (TeX)
        uses: teatimeguest/setup-texlive-action@v3
        with:
          packages: |
            scheme-minimal
            latex-bin
            fontspec
            standalone
            pgf
            pdftexcmds
            luatex85
            infwarerr
            ltxcmds
            xcolor
            fontawesome
            spath3
            inter
            epstopdf-pkg
            tex-gyre
            sourcecodepro

      - name: Install elan
        run: |
          set -o pipefail
          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
          ./elan-init -y --default-toolchain none
          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"

      - uses: actions/checkout@v4

      - name: Lean Version
        run: |
          lean --version

      - name: Cache .lake
        uses: actions/cache@v4
        with:
          path: .lake
          key: ${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('lakefile.lean') }}-${{ github.sha }}
          restore-keys: |
            ${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('lakefile.lean') }}-${{ github.sha }}
            ${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('lakefile.lean') }}
            ${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-
            ${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-

      - name: Build
        run: |
          lake build

      - name: Generate HTML
        run: |
          lake exe generate-manual --depth 2 --with-word-count "words.txt"

      - name: Generate proofreading HTML
        if: github.event_name == 'pull_request'
        run: |
          lake exe generate-manual --depth 2 --with-word-count "words.txt" --draft --output "_out/draft"

      - name: Report word count
        run: |
          echo "Word Counts"
          echo "-----------"
          cat words.txt

      - name: Save word count
        run: |
          echo "# Word Counts" >> $GITHUB_STEP_SUMMARY
          echo "" >> $GITHUB_STEP_SUMMARY
          echo "\`\`\`" >> $GITHUB_STEP_SUMMARY
          cat words.txt >> $GITHUB_STEP_SUMMARY
          echo "\`\`\`" >> $GITHUB_STEP_SUMMARY

      - name: Offline link checker
        uses: lycheeverse/lychee-action@v1.9.0
        with:
          fail: true
          args: --base './_out/html-multi/' --no-progress --offline './_out/html-multi/**/*.html'

      # 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
        with:
          script: |
            if (process.env.PR) {
                return `pr-${process.env.PR}`
            } else {
                return 'deploy-preview-main';
            }
        env:
          PR: ${{ github.event.number }}

        # deploy-info computes metadata that's shown in the Netlify interface
        # about the deployment (for non-PR deploys)
      - id: deploy-info
        name: Compute Deployment Metadata
        if: github.event_name != 'pull_request'
        run: |
          set -e
          echo "message=$(git log -1 --pretty=format:"%s")" >> "$GITHUB_OUTPUT"

      # When a release is created in GH, push to the main site without proofreading info
      - name: Deploy releases when tags are pushed
        id: deploy-release
        uses: nwtgck/actions-netlify@v2.0
        if: github.event_name == 'release'
        with:
          publish-dir: _out/html-multi
          production-branch: main
          production-deploy: true
          github-token: ${{ secrets.GITHUB_TOKEN }}
          deploy-message: |
            Release from tag ${{ github.ref }}
          enable-commit-comment: false
          enable-pull-request-comment: false
          fails-without-credentials: true
        env:
          NETLIFY_AUTH_TOKEN: ${{ secrets.NETLIFY_AUTH_TOKEN }}
          NETLIFY_SITE_ID: "447031bf-9a96-4cee-831b-1f73599a7cb2"

      # When pushing to `main` or a PR branch, deploy what it would look like if this were released
      - name: Deploy current draft
        id: deploy-draft
        uses: nwtgck/actions-netlify@v2.0
        if: github.event_name == 'push' || github.event_name == 'pull_request'
        with:
          publish-dir: _out/html-multi
          production-branch: main
          production-deploy: true
          github-token: ${{ secrets.GITHUB_TOKEN }}
          deploy-message: |
            ${{ github.event_name == 'pull_request' && format('pr#{0}: {1}', github.event.number, github.event.pull_request.title) || format('ref/{0}: {1}', github.ref_name, steps.deploy-info.outputs.message) }}
          alias: ${{ steps.deploy-alias.outputs.result }}
          enable-commit-comment: false
          enable-pull-request-comment: false
          github-deployment-environment: |
            ${{ github.event_name == 'pull_request' && format('lean-ref-pr-#{0}', github.event.number) || '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:
          github.event_name == 'pull_request'
        with:
          publish-dir: _out/draft/html-multi
          production-branch: main
          production-deploy: false
          github-token: ${{ secrets.GITHUB_TOKEN }}
          deploy-message: |
            ${{ github.event_name == 'pull_request' && format('pr#{0} proofreading: {1}', github.event.number, github.event.pull_request.title) }}
          alias: draft-${{ steps.deploy-alias.outputs.result }}
          enable-commit-comment: false
          enable-pull-request-comment: false
          github-deployment-environment: |
            ${{ github.event_name == 'pull_request' && format('lean-ref-pr-draft-#{0}', github.event.number) }}
          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"



  check-links:
    name: Check links
    runs-on: ubuntu-latest
    needs: [build]
    steps:
      - uses: actions/checkout@v4
        with:
          sparse-checkout: |
            .skip-link-check

      - name: Online link checker
        uses: filiph/linkcheck@2.0.23
        continue-on-error: true
        with:
          arguments: --skip-file .skip-link-check -e ${{ needs.build.outputs.ref-url }}