chore: merge main into nightly-testing and bump to 2026-06-22

.github/actions/install-texlive/action.yml

@@ -46,6 +46,11 @@ runs:
                   etoolbox
                   ulem
                   newunicodechar
+                  svg
+                  transparent
+                  trimspaces
+                  xkeyval
+                  catchfile
 
         - name: Check `tlmgr` version
           shell: bash

.github/workflows/actionlint.yml

@@ -7,7 +7,7 @@ jobs:
         name: "Lint GitHub Actions workflows"
         runs-on: ubuntu-latest
         steps:
-            - uses: actions/checkout@v6
+            - uses: actions/checkout@v7
 
             - name: Run actionlint
               uses: reviewdog/action-actionlint@v1

.github/workflows/check-format.yml

@@ -1,4 +1,4 @@
-name: Check Formatting of JS/CSS/HTML and Markdown
+name: Check Code Formatting
 
 on:
     pull_request:
@@ -9,11 +9,23 @@ jobs:
         runs-on: ubuntu-latest
         steps:
             - name: Checkout
-              uses: actions/checkout@v6
+              uses: actions/checkout@v7
 
             - name: Check formatting with prettier
               uses: creyD/prettier_action@v4.6
               with:
                   dry: true
                   prettier_options: "--check ."
                   prettier_version: 3.7.4
+
+    check-python-formatting:
+        runs-on: ubuntu-latest
+        steps:
+            - name: Checkout
+              uses: actions/checkout@v7
+
+            - name: Install uv
+              uses: astral-sh/setup-uv@v7
+
+            - name: Check Python formatting with ruff
+              run: uvx ruff format --check .

.github/workflows/ci.yml

@@ -24,7 +24,7 @@ jobs:
                   ./elan-init -y --default-toolchain none
                   echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
 
-            - uses: actions/checkout@v6
+            - uses: actions/checkout@v7
 
             - name: List all files
               run: |
@@ -63,49 +63,30 @@ jobs:
                   lake build
 
             - name: Install PDF Dependencies
-              uses: zauguin/install-texlive@v4
+              uses: ./.github/actions/install-texlive
+
+            # 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@v5
               with:
-                  packages: |
-                      scheme-minimal
-                      l3packages
-                      tools
-                      latex-bin
-                      xpatch
-                      booktabs
-                      footmisc
-                      environ
-                      hyperref
-                      titlesec
-                      tocloft
-                      enumitem
-                      fmtcount
-                      glossaries
-                      datatool
-                      caption
-                      babel
-                      fontspec
-                      textcase
-                      memoir
-                      sourcecodepro
-                      sourcesans
-                      sourceserif
-                      fvextra
-                      upquote
-                      lineno
-                      float
-                      tcolorbox
-                      tikzfill
-                      pdfcol
-                      listings
-                      epstopdf-pkg
-                      pgf
-                      environ
-                      etoolbox
-                      ulem
-                      newunicodechar
-
-            - name: Check `tlmgr` version
-              run: tlmgr --version
+                  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
+
+            # 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
@@ -125,6 +106,14 @@ jobs:
               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
@@ -184,6 +173,23 @@ jobs:
                   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
@@ -223,9 +229,28 @@ jobs:
               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
@@ -264,7 +289,7 @@ jobs:
 
             - name: Deploy Verso manual
               id: deploy-lang
-              uses: nwtgck/actions-netlify@v3.0
+              uses: nwtgck/actions-netlify@v4.0
               if: github.event_name == 'push' && github.ref_name == 'main'
               with:
                   publish-dir: _out/html-multi

.github/workflows/commit-convention.yml

@@ -11,7 +11,7 @@ jobs:
         runs-on: ubuntu-latest
         steps:
             - name: Check PR title
-              uses: actions/github-script@v8
+              uses: actions/github-script@v9
               with:
                   script: |
                       let title;

.github/workflows/consistent-pr-comment.yml

@@ -0,0 +1,125 @@
+name: Fix toolchain consistency on PR Comment
+
+on:
+    issue_comment:
+        types: [created]
+
+jobs:
+    consistent:
+        # Only run on PR comments containing "!consistent"
+        if: >-
+            github.event.issue.pull_request && contains(github.event.comment.body, '!consistent')
+        runs-on: ubuntu-latest
+        permissions:
+            contents: write
+            pull-requests: write
+        steps:
+            - name: Check user permission
+              uses: actions/github-script@v9
+              with:
+                  script: |
+                      const { data: permission } = await github.rest.repos.getCollaboratorPermissionLevel({
+                        owner: context.repo.owner,
+                        repo: context.repo.repo,
+                        username: context.payload.comment.user.login
+                      });
+                      const level = permission.permission;
+                      if (level !== 'admin' && level !== 'write') {
+                        core.setFailed(
+                          `User ${context.payload.comment.user.login} does not have write access (permission: ${level})`
+                        );
+                      }
+
+            - name: Get PR details
+              id: pr-details
+              uses: actions/github-script@v9
+              with:
+                  script: |
+                      const { data: pr } = await github.rest.pulls.get({
+                        owner: context.repo.owner,
+                        repo: context.repo.repo,
+                        pull_number: context.payload.issue.number
+                      });
+                      const isFork = pr.head.repo.full_name !== `${context.repo.owner}/${context.repo.repo}`;
+                      if (isFork && !pr.maintainer_can_modify) {
+                        core.setFailed(
+                          'Cannot push to this fork PR. The PR author must enable "Allow edits by maintainers".'
+                        );
+                      }
+
+            - name: Add reaction to acknowledge
+              uses: actions/github-script@v9
+              with:
+                  script: |
+                      await github.rest.reactions.createForIssueComment({
+                        owner: context.repo.owner,
+                        repo: context.repo.repo,
+                        comment_id: context.payload.comment.id,
+                        content: 'eyes'
+                      });
+
+            - name: Checkout repository
+              uses: actions/checkout@v7
+              with:
+                  token: ${{ secrets.GITHUB_TOKEN }}
+
+            - name: Checkout PR branch
+              env:
+                  GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+              run: gh pr checkout ${{ github.event.issue.number }}
+
+            - name: Sync test-project lean-toolchains
+              run: |
+                  targets=(
+                    test-projects/literate-config/lean-toolchain
+                    test-projects/literate-multi-root/lean-toolchain
+                  )
+                  for t in "${targets[@]}"; do
+                    if [ -L "$t" ]; then
+                      echo "Refusing to write through symlink: $t"
+                      exit 1
+                    fi
+                  done
+                  for t in "${targets[@]}"; do
+                    cp lean-toolchain "$t"
+                  done
+
+            - name: Commit and push
+              id: commit
+              run: |
+                  git config user.name "github-actions[bot]"
+                  git config user.email "github-actions[bot]@users.noreply.github.com"
+                  git add -- \
+                    test-projects/literate-config/lean-toolchain \
+                    test-projects/literate-multi-root/lean-toolchain
+                  if git diff --cached --quiet; then
+                    echo "No consistency fixes needed"
+                    echo "changes=false" >> "$GITHUB_OUTPUT"
+                  else
+                    git commit -m "ci: sync test-project lean-toolchains"
+                    git push
+                    echo "changes=true" >> "$GITHUB_OUTPUT"
+                  fi
+
+            - name: Add completion reaction
+              uses: actions/github-script@v9
+              with:
+                  script: |
+                      await github.rest.reactions.createForIssueComment({
+                        owner: context.repo.owner,
+                        repo: context.repo.repo,
+                        comment_id: context.payload.comment.id,
+                        content: '${{ steps.commit.outputs.changes == 'true' && 'rocket' || '+1' }}'
+                      });
+
+            - name: Add failure reaction
+              if: failure()
+              uses: actions/github-script@v9
+              with:
+                  script: |
+                      await github.rest.reactions.createForIssueComment({
+                        owner: context.repo.owner,
+                        repo: context.repo.repo,
+                        comment_id: context.payload.comment.id,
+                        content: 'confused'
+                      });

.github/workflows/consistent-subverso-manifests.yml

@@ -12,7 +12,7 @@ jobs:
         name: SubVerso version consistency
         runs-on: ubuntu-latest
         steps:
-            - uses: actions/checkout@v6
+            - uses: actions/checkout@v7
 
             - name: Check for consistent Subverso versions in all manifests
               run: |
@@ -65,5 +65,7 @@ jobs:
                     fi
                   done
                   if [ "$FAILED" -ne 0 ]; then
+                    echo ""
+                    echo "To fix automatically, comment '!consistent' on the PR."
                     exit 1
                   fi

.github/workflows/copyright-header.yml

@@ -7,7 +7,7 @@ jobs:
         name: "Check copyright header and Lean import size"
         runs-on: ubuntu-latest
         steps:
-            - uses: actions/checkout@v6
+            - uses: actions/checkout@v7
 
             - name: Don't 'import Lean', use precise imports
               run: |

.github/workflows/dependabot-clean-description.yml

@@ -15,7 +15,7 @@ jobs:
             - run: npm install marked@latest
 
             - name: Rewrite PR description and post original as comment
-              uses: actions/github-script@v8
+              uses: actions/github-script@v9
               with:
                   script: |
                       const { marked } = require('marked');