ci.yml

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

name: "Build and check HTML"

jobs:
  build:
    name: Build site and generate HTML
    runs-on: ubuntu-latest

    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
            lualatex-math
            infwarerr
            ltxcmds
            xcolor
            fontawesome
            spath3
            inter
            epstopdf-pkg
            tex-gyre
            tex-gyre-math
            unicode-math
            amsmath
            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/restore@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 figures
        run: |
          lake build figures

      - name: Build
        run: |
          lake build

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

      - name: Generate HTML (non-release)
        if: github.event_name != 'release'
        run: |
          lake --quiet exe generate-manual --depth 2 --with-word-count "words.txt" --verbose --without-html-single

      - name: Generate HTML (release)
        if: github.event_name == 'release'
        # Include the base to fix trailing slash issue on Netlify
        run: |
          lake --quiet exe generate-manual --depth 2 --with-word-count "words.txt" --verbose --site-base-url "/doc/reference/latest/"

      - name: Generate proofreading HTML
        if: github.event_name == 'pull_request'
        run: |
          lake --quiet exe generate-manual --depth 2 --verbose --draft --without-html-single --output "_out/draft"

      - name: Save generated HTML to artifact storage
        uses: actions/upload-artifact@v4
        with:
          name: 'html'
          path: '_out/'
          retention-days: 5
          overwrite: true

      - 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 (non-release)
        uses: lycheeverse/lychee-action@v1.9.0
        if: github.event_name == 'push' || github.event_name == 'pull_request'
        with:
          fail: true
          args: --base './_out/html-multi/' --no-progress --offline './_out/html-multi/**/*.html'

      # This saved number is used by a workflow_run trigger. It
      # manages labels that indicate the status of the built HTML.
      - name: Save PR number
        if: github.event_name == 'pull_request'
        run: |
          mkdir -p ./pr
          echo ${{ github.event.number }} > ./pr/NR
      - uses: actions/upload-artifact@v4
        if: github.event_name == 'pull_request'
        with:
          name: pr
          path: pr/

  deploy:
    name: Deploy release
    runs-on: ubuntu-latest
    needs: [build]
    if: github.event_name == 'release'
    outputs:
      ref-url: ${{ steps.deploy-release.outputs.deploy-url }}
    steps:
      - name: Get generated HTML from artifact storage
        uses: actions/download-artifact@v4
        with:
          name: 'html'
          path: '_out/'

      # 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"


  check-links:
    name: Check links
    runs-on: ubuntu-latest
    needs: [deploy]
    if: github.event_name == 'release'
    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.deploy.outputs.ref-url }}

  prose-lint:
    name: Check prose
    runs-on: ubuntu-latest
    needs: [build]
    steps:
      - uses: actions/checkout@v4

      - name: Get generated HTML from artifact storage
        uses: actions/download-artifact@v4
        with:
          name: 'html'
          path: '_out/'

      - name: Install prose linter
        run: |
          sudo snap install vale

      - name: Preprocess HTML for prose linter
        run: |
          # First the HTML needs preprocessing to work well with Vale
          pushd _out
          python3 -m venv venv
          . venv/bin/activate
          pip install beautifulsoup4
          python ../.vale/scripts/rewrite_html.py html-multi html-vale
          popd

      - name: Prose linter
        run: |
          set -o pipefail
          vale --output JSON _out/html-vale/ | python .vale/scripts/report.py