ci.yml

on:
  push:
    branches:
      - main
  pull_request:
  workflow_dispatch:

permissions:
  contents: read
  pages: write
  id-token: write

concurrency:
  group: "pages"
  cancel-in-progress: false

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
            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/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
        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'

      - name: Upload artifact
        uses: actions/upload-pages-artifact@v3
        with:
          path: _out/html-multi
  
  # Deployment job
  deploy:
    if: github.ref == 'refs/heads/main'
    environment:
      name: github-pages
      url: ${{ steps.deployment.outputs.page_url }}
    runs-on: ubuntu-latest
    needs: build
    steps:
      - name: Deploy to GitHub Pages
        id: deployment
        uses: actions/deploy-pages@v4
  

  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