ci.yml

on:
    push:
        branches:
            - master
            - main
            - nightly-testing
    pull_request:
    merge_group:

name: Continuous Integration

jobs:
    build:
        name: Build and test
        runs-on: nscloud-ubuntu-22.04-amd64-8x16
        env:
            # Used for browser tests. Placing them here allows caching to work right.
            PLAYWRIGHT_BROWSERS_PATH: ${{ github.workspace }}/.playwright-browsers
        steps:
            - 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@v7

            - name: Install subproject toolchains
              run: |
                  find . -name lean-toolchain -type f -not -path './.*' | while read -r f; do
                      elan toolchain install "$(cat "$f")"
                  done

            - name: List all files
              run: |
                  find . -name "*.lean" -type f

            - name: lean version
              run: |
                  lean --version

            - name: Compute short SHA
              id: shortSHA
              run: echo "short_sha=$(git rev-parse --short HEAD)" >> "$GITHUB_OUTPUT"

            - name: Cache .lake
              uses: actions/cache@v6
              with:
                  path: .lake
                  # The SHA is in the key to get the most recent cache possible, rather than just saving a single one for each Lean/deps version and not touching it.
                  key:
                      ${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{
                      hashFiles('lean-toolchain') }}-${{ steps.shortSHA.outputs.short_sha }}
                  # Try to restore cache for same OS/Lean/deps, but don't get less specific, because Lake isn't always happy to get build product version mismatches
                  restore-keys: |
                      ${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('lean-toolchain') }}-

            # This was failing CI from clang crashing, so do it first for fast turnaround
            - name: Build the website examples subproject
              run: |
                  pushd test-projects/website-examples
                  lake build
                  lake build :examples
                  popd

            - name: Build the project
              run: |
                  lake build

            - name: Install PDF Dependencies
              uses: ./.github/actions/install-texlive

            # Inkscape is needed by the LaTeX `svg` package, which converts
            # SVG files emitted by `diagram` code blocks to PDF at build time.
            - name: Install Inkscape
              run: sudo apt-get update && sudo apt-get install -y --no-install-recommends inkscape

            # Install uv and Playwright before tests, since lake test
            # runs literate browser tests that need them
            - name: Install uv
              uses: astral-sh/setup-uv@v7
              with:
                  enable-cache: true
                  cache-dependency-glob: "browser-tests/pyproject.toml"

            - name: Cache Playwright browsers
              uses: actions/cache@v6
              with:
                  path: .playwright-browsers
                  key: playwright-${{ runner.os }}-${{ hashFiles('browser-tests/uv.lock') }}

            - name: Install Playwright browsers
              run: |
                  uv run --project browser-tests --extra test playwright install chromium firefox --with-deps

            # The LaTeX `svg` package shells out to `inkscape --version` during
            # the `--check-tex` build. Fail here with a clear message if Inkscape
            # is missing or its version can't be read, rather than deep inside a
            # lualatex run.
            - name: Check Inkscape is available
              run: |
                  inkscape --version

            - name: Run tests
              run: |
                  lake test -- --verbose --check-tex

            - name: Test the dev server
              run: |
                  ./src/tests/run_serve_test.sh

            - name: Generate the test website
              run: |
                  lake exe demosite --output _out/test-projects/demosite

            - name: Generate the test genre's document
              run: |
                  lake exe simplepage

            - name: Generate some source HTML
              run: |
                  lake build Verso.Hover:literate
                  lake exe verso-html .lake/build/literate htmlout

            - name: Install linkchecker
              run: pip install linkchecker

            - name: Check internal links on the test website
              run: |
                  linkchecker --config=.linkchecker/linkcheckerrc --no-status ./_out/test-projects/demosite/

            - name: Generate the test tutorial site
              run: |
                  lake exe tutorial-example

            - name: Check internal links on the test tutorial site
              run: |
                  linkchecker --config=.linkchecker/linkcheckerrc --no-status ./_out/tut/

            - name: Generate the manual
              run: |
                  ./generate.sh
                  cp _out/tex/main.pdf ./manual.pdf
                  cp -r _out/html-multi html-multi
                  cp README-html.md html-multi/README.md
                  zip -r html-manual.zip html-multi

            - uses: actions/setup-node@v7
              with:
                  node-version: "lts/*"
                  cache: npm

            - run: npm ci

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

            - name: Type check the xref redirect JS code
              run: |
                  pushd static-web
                  npx tsc --noEmit -p jsconfig.json
                  popd

            - name: Check the ToC width storage key stays in sync
              run: |
                  # toc-resize.js and toc-resize-preload.js must agree on the localStorage
                  # key, since the preload primes the value the main script later reads.
                  main_key=$(grep -oE 'STORAGE_KEY = "[^"]+"' static-web/toc-resize.js | grep -oE '"[^"]+"')
                  preload_key=$(grep -oE 'getItem\("[^"]+"\)' static-web/toc-resize-preload.js | grep -oE '"[^"]+"')
                  echo "toc-resize.js storage key:         ${main_key:-<none>}"
                  echo "toc-resize-preload.js storage key: ${preload_key:-<none>}"
                  if [ -z "$main_key" ] || [ -z "$preload_key" ]; then
                      echo "::error::Could not find the ToC width storage key in one of the scripts" >&2
                      exit 1
                  fi
                  if [ "$main_key" != "$preload_key" ]; then
                      echo "::error::ToC width localStorage key differs between toc-resize.js and toc-resize-preload.js" >&2
                      exit 1
                  fi

            - name: Generate the demo site and make sure page_link works
              run: |
                  lake exe demosite --output _out/demosite
                  # Fail if the generated about page doesn't have the expected base tag and blog link
                  grep -qF '<a href="blog/">blog</a> genre' _out/demosite/about/index.html
                  grep -qF '<base href=".././">' _out/demosite/about/index.html

            # uv and Playwright are installed before `lake test` above.
            - name: Cache literate-config test project
              uses: actions/cache@v6
              with:
                  path: test-projects/literate-config/.lake
                  key:
                      literate-config-${{ runner.os }}-${{
                      hashFiles('test-projects/literate-config/lean-toolchain') }}-${{
                      hashFiles('test-projects/literate-config/lake-manifest.json') }}-${{
                      steps.shortSHA.outputs.short_sha }}
                  restore-keys: |
                      literate-config-${{ runner.os }}-${{ hashFiles('test-projects/literate-config/lean-toolchain') }}-${{ hashFiles('test-projects/literate-config/lake-manifest.json') }}-

            - name: Cache literate-multi-root test project
              uses: actions/cache@v6
              with:
                  path: test-projects/literate-multi-root/.lake
                  key:
                      literate-multi-root-${{ runner.os }}-${{
                      hashFiles('test-projects/literate-multi-root/lean-toolchain') }}-${{
                      hashFiles('test-projects/literate-multi-root/lake-manifest.json') }}-${{
                      steps.shortSHA.outputs.short_sha }}
                  restore-keys: |
                      literate-multi-root-${{ runner.os }}-${{ hashFiles('test-projects/literate-multi-root/lean-toolchain') }}-${{ hashFiles('test-projects/literate-multi-root/lake-manifest.json') }}-

            - name: Run literate browser tests
              run: src/tests/run_literate_browser_tests.sh

            - name: Run browser tests
              run: |
                  uv run --project browser-tests --extra test pytest \
                    browser-tests/test_search.py \
                    browser-tests/test_search_priority.py \
                    browser-tests/test_search_page.py \
                    browser-tests/test_toc_resize.py \
                    browser-tests/test_redirect.py \
                    browser-tests/test_katex.py -v

            - name: Build the VersoHtml site for browser tests
              run: |
                  # The verso-html genre renders literate JSON into a standalone HTML site.
                  # We reuse the literate-config test project (already cached) as input, then
                  # run verso-html against its literate-JSON output.
                  pushd test-projects/literate-config
                  lake build +LitConfig:literate
                  popd
                  lake exe verso-html test-projects/literate-config/.lake/build/literate _out/verso-html

            - name: Run VersoHtml browser tests
              run: |
                  uv run --project browser-tests --extra test pytest \
                    browser-tests/verso-html -v \
                    --site-dir "$(pwd)/_out/verso-html"

            - name: Upload docs to artifact storage
              if: github.ref != 'refs/heads/main'
              uses: actions/upload-artifact@v7
              with:
                  name: "Verso manual (PDF and HTML)"
                  path: |
                      manual.pdf
                      html-manual.zip

            - uses: "marvinpinto/action-automatic-releases@v1.2.1"
              if: github.ref == 'refs/heads/main'
              with:
                  repo_token: "${{ secrets.GITHUB_TOKEN }}"
                  automatic_release_tag: "latest"
                  title: "Verso manual (PDF and HTML)"
                  files: |
                      manual.pdf
                      html-manual.zip

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

            - name: Upload HTML manual for PR deployment
              if: github.event_name == 'pull_request'
              uses: actions/upload-artifact@v7
              with:
                  name: html-manual-for-deploy
                  path: _out/html-multi
                  retention-days: 1

            - name: Deploy Verso manual
              id: deploy-lang
              uses: nwtgck/actions-netlify@v4.0
              if: github.event_name == 'push' && github.ref_name == 'main'
              with:
                  publish-dir: _out/html-multi
                  production-branch: main
                  github-token: ${{ secrets.GITHUB_TOKEN }}
                  alias: ref-${{ github.ref_name }}
                  deploy-message:
                      "ref/${{ github.ref_name }}: ${{ steps.deploy-info.outputs.message }}"
                  enable-commit-comment: false
                  github-deployment-environment: verso-main
                  fails-without-credentials: true
              env:
                  NETLIFY_AUTH_TOKEN: ${{ secrets.NETLIFY_AUTH_TOKEN }}
                  NETLIFY_SITE_ID: "8a89abd8-095b-4496-a9c1-381d2d5629ec" # TODO: if a tag, push to a different site for hosting under lean-lang.org