on:
    push:
        branches:
            - main
            - nightly-testing
            - "lean-pr-testing-*"
    pull_request:
        branches:
            - main
            - nightly-testing
    merge_group:
    release:
        types:
            - published
            - released

name: "Build and check HTML"

jobs:
    build:
        name: Build site and generate HTML
        runs-on: nscloud-ubuntu-22.04-amd64-8x16

        steps:
            - name: Display usage limits
              run: |
                  ulimit -a

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

            - name: Install deps for figures (TeX)
              uses: zauguin/install-texlive@v4
              with:
                  texlive_version: 2025
                  packages: |
                      scheme-small
                      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: Do we have lualatex?
              run: |
                  lualatex --version

            - name: Install elan
              run: |
                  set -o pipefail
                  curl -sSfL https://github.com/leanprover/elan/releases/download/v4.1.2/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/packages
                      .lake/build/bin
                      .lake/build/ir
                      .lake/build/lib
                  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
              id: build
              run: |
                  lake --no-ansi build 2>&1 | tee build.log
            - name: Generate build time summary
              if: always() # Run even if build fails
              run: |
                  # Create build times summary
                  echo "## Build Times Summary" >> $GITHUB_STEP_SUMMARY
                  echo "" >> $GITHUB_STEP_SUMMARY
                  echo "Sorted by build time (longest first):" >> $GITHUB_STEP_SUMMARY
                  echo "" >> $GITHUB_STEP_SUMMARY
                  echo "| Component | Time |" >> $GITHUB_STEP_SUMMARY
                  echo "|-----------|------|" >> $GITHUB_STEP_SUMMARY

                  # Parse build output, convert times to seconds for sorting, then sort
                  if [ -f build.log ]; then
                  # Create temporary Python script
                  cat > parse_times.py << 'EOF'
                  import sys
                  import re

                  def time_to_seconds(time_str):
                      if 'ms' in time_str:
                          return float(time_str.replace('ms', '')) / 1000
                      elif 's' in time_str:
                          return float(time_str.replace('s', ''))
                      return 0

                  lines = []
                  for line in sys.stdin:
                      time_str, component = line.strip().split('|', 1)
                      seconds = time_to_seconds(time_str)
                      lines.append((seconds, time_str, component.strip()))

                  lines.sort(reverse=True)

                  for _, time_str, component in lines:
                      print(f'| {component} | {time_str} |')
                  EOF

                    grep "[✔⚠].*Built.*(" build.log | \
                    sed -E 's/.*Built ([^(]+) \(([^)]+)\).*/\2|\1/' | \
                    python3 parse_times.py >> $GITHUB_STEP_SUMMARY

                    rm parse_times.py
                  else
                    echo "No build log found" >> $GITHUB_STEP_SUMMARY
                  fi

            - name: Save cache for .lake
              uses: actions/cache/save@v4
              with:
                  path: |
                      .lake/packages
                      .lake/build/bin
                      .lake/build/ir
                      .lake/build/lib
                  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'
              run: |
                  lake --quiet exe generate-manual --depth 2 --with-word-count "words.txt" --verbose --without-html-single

            - name: Check Manual Examples are Isolated
              run: |
                  scripts/check-examples-isolated.sh

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

            - name: Report status to Lean PR
              if: always() && github.repository == 'leanprover/reference-manual'
              shell: bash
              env:
                  TOKEN: ${{ secrets.LEAN_PR_TESTING }}
                  GITHUB_CONTEXT: ${{ toJson(github) }}
                  WORKFLOW_URL:
                      https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}
                  BUILD_OUTCOME: ${{ steps.build.outcome }}
                  GENERATE_OUTCOME: ${{ steps.generate.outcome }}
                  NIGHTLY_TESTING_REPO: leanprover/reference-manual
              run: |
                  scripts/lean-pr-testing-comments.sh lean

            - 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: Set up Python for link checker
              if: github.event_name == 'push' || github.event_name == 'pull_request'
              uses: actions/setup-python@v4
              with:
                  python-version: "3.10"

            - name: Install LinkChecker
              if: github.event_name == 'push' || github.event_name == 'pull_request'
              run: |
                  python -m pip install --upgrade pip
                  pip install linkchecker

            - name: Run LinkChecker (local links only)
              if: github.event_name == 'push' || github.event_name == 'pull_request'
              run: |
                  linkchecker --config=.linkchecker/linkcheckerrc './_out/html-multi/'

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

    preview:
        name: Deploy preview
        runs-on: ubuntu-latest
        needs: [build]
        if: github.event_name == 'push' && github.ref_name == 'nightly-testing'
        steps:
            - name: Get generated HTML from artifact storage
              uses: actions/download-artifact@v4
              with:
                  name: "html"
                  path: "_out/"

            - name: Deploy current draft
              id: deploy-draft
              uses: nwtgck/actions-netlify@v2.0
              with:
                  publish-dir: _out/html-multi
                  production-branch: main
                  production-deploy: true
                  github-token: ${{ secrets.GITHUB_TOKEN }}
                  deploy-message: |
                      ${{ format('preview of {0}', github.ref) }}
                  enable-commit-comment: false
                  enable-pull-request-comment: false
                  github-deployment-description: |
                      Latest draft (without 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: [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

    type-check-js:
        name: Check search JS code with TypeScript
        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 TypeScript
              run: |
                  sudo apt update && sudo apt install node-typescript

            - name: Type check the search bar code
              run: |
                  cd _out/html-multi/-verso-search
                  tsc --noEmit -p jsconfig.json