@@ -1,312 +1,46 @@
 name: tests
 
 on:
-  # main tests each merged commit. scratch/ branches run CI on a branch with no
-  # pull request; every other branch runs through pull_request.
   push:
-    branches: [main, "scratch/**"]
-  pull_request:
+    branches: ["scratch/**"]
 
 permissions:
   contents: read
 
-# A newer commit on a pull request cancels the run for the older one. Each push
-# gets a group of its own: runs that share a group wait one at a time, and a
-# newer one cancels any still waiting, so runs on main would skip commits.
-concurrency:
-  group: tests-${{ github.event.pull_request.number || github.run_id }}
-  cancel-in-progress: ${{ github.event_name == 'pull_request' }}
-
 jobs:
-  test:
-    runs-on: ubuntu-latest
-    timeout-minutes: 30
-    strategy:
-      matrix:
-        python-version: ["3.10", "3.13"]
-    steps:
-      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
-      - uses: actions/setup-node@249970729cb0ef3589644e2896645e5dc5ba9c38 # v6
-        with:
-          node-version: "22.23.2"
-      - name: Install pinned explorer compiler
-        run: |
-          timeout --signal=TERM --kill-after=30s 3m npm ci --ignore-scripts --no-audit --no-fund --prefer-offline \
-            --fetch-timeout=30000 --fetch-retries=2 --fetch-retry-mintimeout=2000 --fetch-retry-maxtimeout=10000
-      - run: npm run check:explorer
-      - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0
-        with:
-          version: "0.12.1"
-          python-version: ${{ matrix.python-version }}
-          enable-cache: true
-      - run: uv sync --extra dev --extra repl
-      - run: uv run ruff check autoform_cli servers tests
-      - run: uv run pytest -q
-      - run: make check-example
-
-  browser:
-    name: WebKit integrated book and explorer regressions
+  atlas:
+    name: ATLAS screenshots
     runs-on: ubuntu-latest
-    timeout-minutes: 25
+    timeout-minutes: 45
     steps:
       - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
       - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0
         with:
           version: "0.12.1"
           python-version: "3.13"
           enable-cache: true
-      - name: Install locked browser test environment
-        run: uv sync --frozen --extra dev --extra browser
-      - name: Install WebKit and Linux system dependencies
-        run: uv run --frozen --extra browser playwright install --with-deps webkit
-      - name: Run integrated book, explorer and genuine MathJax regressions
+      - run: uv sync --frozen --extra dev --extra browser
+      - run: uv run --frozen --extra browser playwright install --with-deps webkit
+      - name: Clone the ATLAS wiki
+        run: |
+          git clone --depth 1 --filter=blob:none --sparse --branch wiki/autoform-blueprint https://github.com/Deicyde/atlas-lean.git atlas
+          git -C atlas sparse-checkout set --no-cone '/*' '!/v1/'
+          git -C atlas log -1 --format='atlas %h %s'
+      - name: Render
+        run: uv run --frozen python -m autoform_cli render atlas/blueprint --output atlas/site-src --lean-root atlas
+      - name: Build
+        working-directory: atlas
         run: >-
-          uv run --frozen --extra dev --extra browser pytest -q
-          tests/test_dag_viewer_browser.py tests/test_integrated_explorer_browser.py
-          tests/test_integrated_workspace_browser.py tests/test_integrated_continuity_browser.py
-        env:
-          AUTOFORM_REQUIRE_BROWSER_TESTS: "1"
-          AUTOFORM_UI_SCREENSHOT_DIR: ${{ runner.temp }}/autoform-ui-evidence
-      - name: Preserve browser UI screenshots and diagnostics
+          uvx --from mkdocs==1.6.1 --with mkdocs-material==9.6.21
+          --with mkdocs-literate-nav==0.6.2 --with pymdown-extensions==10.21.3
+          mkdocs build --strict
+      - name: Screenshot
+        run: |
+          (cd atlas/site && python3 -m http.server 8765 --bind 127.0.0.1 > /dev/null 2>&1 &)
+          sleep 2
+          uv run --frozen --extra browser python .scratch/atlas_shots.py
+      - uses: actions/upload-artifact@v4
         if: always()
-        uses: actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9 # v7
-        with:
-          name: integrated-ui-evidence-${{ github.run_id }}
-          path: ${{ runner.temp }}/autoform-ui-evidence
-          if-no-files-found: warn
-          retention-days: 7
-
-  mathjax:
-    name: MathJax read-back cards (Node)
-    runs-on: ubuntu-latest
-    timeout-minutes: 15
-    steps:
-      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
-      - uses: actions/setup-node@249970729cb0ef3589644e2896645e5dc5ba9c38 # v6
-        with:
-          node-version: "22.23.2"
-      - name: Install locked native DOM test bridge
-        run: |
-          timeout --signal=TERM --kill-after=30s 3m npm ci --ignore-scripts --no-audit --no-fund --prefer-offline \
-            --fetch-timeout=30000 --fetch-retries=2 --fetch-retry-mintimeout=2000 --fetch-retry-maxtimeout=10000
-      - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0
-        with:
-          version: "0.12.1"
-          python-version: "3.13"
-          enable-cache: true
-      - name: Install locked development environment
-        run: uv sync --frozen --extra dev
-      # The npm tarball of the release the site loads, checked against the
-      # sha256 of the one whose sha1 and sha512 npm publishes.
-      - name: Install pinned MathJax 3.2.2
-        run: |
-          set -euo pipefail
-          timeout --signal=TERM --kill-after=15s 2m curl -sSfL \
-            https://registry.npmjs.org/mathjax/-/mathjax-3.2.2.tgz -o mathjax.tgz
-          echo "1b9c0a1c44df864e915690558e72adb9cc5203360daefd385084ced3b6c64c09  mathjax.tgz" \
-            | sha256sum --check --strict
-          mkdir mathjax
-          tar xzf mathjax.tgz -C mathjax
-          echo "AUTOFORM_MATHJAX_DIR=$PWD/mathjax/package" >> "$GITHUB_ENV"
-      - name: Typeset read-back cards in Node with the script render writes
-        run: uv run --frozen --extra dev pytest -q tests/test_site_mathjax_node.py
-        env:
-          AUTOFORM_REQUIRE_MATHJAX_TESTS: "1"
-
-  real-lean:
-    name: real Lean (fixture toolchain)
-    runs-on: ubuntu-latest
-    timeout-minutes: 75
-    steps:
-      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
-      - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0
         with:
-          version: "0.12.1"
-          python-version: "3.13"
-          enable-cache: true
-      - name: Install locked development environment
-        run: timeout --signal=TERM --kill-after=30s 3m uv sync --frozen --extra dev --extra repl
-      - name: Install pinned Elan
-        run: |
-          set -euo pipefail
-          timeout --signal=TERM --kill-after=15s 2m curl -sSfL \
-            https://github.com/leanprover/elan/releases/download/v4.2.3/elan-x86_64-unknown-linux-gnu.tar.gz \
-            -o elan.tar.gz
-          echo "df0b2b3a439961ffcbb3985214365ffe40f49bc871df04dff268c7d8e21ca8b2  elan.tar.gz" \
-            | sha256sum --check --strict
-          tar xzf elan.tar.gz
-          ./elan-init -y --default-toolchain none
-          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
-      - name: Install the fixture's Lean toolchain
-        run: |
-          set -euo pipefail
-          timeout --signal=TERM --kill-after=30s 10m \
-            elan toolchain install "$(tr -d '\r\n' < tests/fixtures/skeleton-project/lean-toolchain)"
-          command -v lake
-      - name: Install the library fixture's Lean toolchain
-        run: |
-          set -euo pipefail
-          timeout --signal=TERM --kill-after=30s 10m \
-            elan toolchain install "$(tr -d '\r\n' < tests/fixtures/library-project/lean-toolchain)"
-      - name: Build a project from the bundled creation release
-        run: |
-          set -euo pipefail
-          generated_project="$RUNNER_TEMP/autoform-created-project"
-          uv run autoform project new "$generated_project" \
-            --package GeneratedProject \
-            --release lean-v4.32.2-mathlib-v4.32.2
-          cd "$generated_project"
-          timeout --signal=TERM --kill-after=30s 20m lake exe cache get
-          timeout --signal=TERM --kill-after=30s 10m lake build
-      - name: Audit the created project as its workflow does
-        run: |
-          set -euo pipefail
-          # The template's helper, so the step audits this checkout's probe on a
-          # build that imports all of Mathlib.
-          helper="$PWD/autoform_cli/templates/github/autoform_audit.py"
-          archive="$RUNNER_TEMP/autoform-created-root.tgz"
-          probe="$RUNNER_TEMP/autoform-created-probe.lean"
-          output="$RUNNER_TEMP/autoform-created-probe.out"
-          cd "$RUNNER_TEMP/autoform-created-project"
-          lake pack "$archive"
-          python3 "$helper" GeneratedProject "$archive" "$probe"
-          lean_path="$(lake env printenv LEAN_PATH)"
-          AUTOFORM_AUDIT_LEAN_PATH="$lean_path" LEAN_ABORT_ON_PANIC=1 \
-            timeout --signal=TERM --kill-after=30s 15m lean "$probe" | tee "$output"
-          if ! tail -n 1 "$output" | grep -Eq '^kernel trust clean \('; then
-            echo "the audit probe did not end with its success line" >&2
-            exit 1
-          fi
-      - name: Run the impact probe against real Lean
-        run: timeout --signal=TERM --kill-after=30s 10m uv run pytest -q tests/test_impact.py
-        env:
-          AUTOFORM_REQUIRE_REAL_LEAN_TESTS: "1"
-      - name: Run the library index generator against real Lean
-        run: timeout --signal=TERM --kill-after=30s 30m uv run pytest -q tests/test_library_generate.py
-        env:
-          AUTOFORM_REQUIRE_REAL_LIBRARY_TESTS: "1"
-      - name: Run the open-statement audit and contract against real Lean
-        run: timeout --signal=TERM --kill-after=30s 10m uv run pytest -q tests/test_lake_artifact_audit.py tests/test_contract.py
-        env:
-          AUTOFORM_REQUIRE_REAL_LEAN_TESTS: "1"
-      - name: Run the LSP lifecycle and diagnostics checks against real Lean
-        run: >-
-          timeout --signal=TERM --kill-after=30s 10m uv run pytest -q -k real_lean
-          tests/test_lsp_protocol.py tests/test_batch_diagnostics.py
-        env:
-          AUTOFORM_REQUIRE_REAL_LEAN_TESTS: "1"
-          AUTOFORM_REAL_LEAN_MATHLIB_PROJECT: ${{ runner.temp }}/autoform-created-project
-
-  real-lean-skeleton:
-    name: real Lean skeleton suite (fixture toolchain)
-    runs-on: ubuntu-latest
-    timeout-minutes: 40
-    steps:
-      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
-      - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0
-        with:
-          version: "0.12.1"
-          python-version: "3.13"
-          enable-cache: true
-      - name: Install locked development environment
-        run: timeout --signal=TERM --kill-after=30s 3m uv sync --frozen --extra dev --extra repl
-      - name: Install pinned Elan
-        run: |
-          set -euo pipefail
-          timeout --signal=TERM --kill-after=15s 2m curl -sSfL \
-            https://github.com/leanprover/elan/releases/download/v4.2.3/elan-x86_64-unknown-linux-gnu.tar.gz \
-            -o elan.tar.gz
-          echo "df0b2b3a439961ffcbb3985214365ffe40f49bc871df04dff268c7d8e21ca8b2  elan.tar.gz" \
-            | sha256sum --check --strict
-          tar xzf elan.tar.gz
-          ./elan-init -y --default-toolchain none
-          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
-      - name: Install the fixture's Lean toolchain
-        run: |
-          set -euo pipefail
-          timeout --signal=TERM --kill-after=30s 10m \
-            elan toolchain install "$(tr -d '\r\n' < tests/fixtures/skeleton-project/lean-toolchain)"
-          command -v lake
-      - name: Run the skeleton suite against real Lean
-        run: >-
-          timeout --signal=TERM --kill-after=30s 35m uv run pytest -q
-          tests/test_skeleton.py
-          tests/test_project_inspect.py::test_stale_inherited_mathlib_is_ignored_by_real_lake
-        env:
-          AUTOFORM_REQUIRE_REAL_LEAN_TESTS: "1"
-
-  real-repl:
-    name: real REPL (fixture toolchain)
-    runs-on: ubuntu-latest
-    timeout-minutes: 15
-    steps:
-      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
-      - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0
-        with:
-          version: "0.12.1"
-          python-version: "3.13"
-          enable-cache: true
-      - name: Install pinned Elan
-        run: |
-          set -euo pipefail
-          timeout --signal=TERM --kill-after=15s 2m curl -sSfL \
-            https://github.com/leanprover/elan/releases/download/v4.2.3/elan-x86_64-unknown-linux-gnu.tar.gz \
-            -o elan.tar.gz
-          echo "df0b2b3a439961ffcbb3985214365ffe40f49bc871df04dff268c7d8e21ca8b2  elan.tar.gz" \
-            | sha256sum --check --strict
-          tar xzf elan.tar.gz
-          ./elan-init -y --default-toolchain none
-          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
-      - name: Build the REPL fixture
-        working-directory: tests/fixtures/repl-smoke
-        run: |
-          set -euo pipefail
-          timeout --signal=TERM --kill-after=30s 5m \
-            elan toolchain install "$(tr -d '\r\n' < lean-toolchain)"
-          timeout --signal=TERM --kill-after=30s 8m lake build Mathlib Secret @repl/repl
-      - name: Install the minimum supported Lean toolchain
-        run: |
-          set -euo pipefail
-          timeout --signal=TERM --kill-after=30s 5m \
-            elan toolchain install "$(tr -d '\r\n' < tests/fixtures/minimum-lean/lean-toolchain)"
-      - name: Install locked development environment
-        run: timeout --signal=TERM --kill-after=30s 3m uv sync --frozen --extra dev --extra repl
-      - name: Run the REPL suite against the pinned upstream REPL
-        run: timeout --signal=TERM --kill-after=30s 10m uv run pytest -q tests/test_real_repl.py
-        env:
-          AUTOFORM_RUN_REAL_REPL_TESTS: "1"
-
-  windows-hardening:
-    name: Windows inspection, subprocess, and publication hardening
-    runs-on: windows-latest
-    timeout-minutes: 15
-    steps:
-      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
-      - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0
-        with:
-          version: "0.12.1"
-          python-version: "3.13"
-          enable-cache: true
-      - run: uv sync --frozen --extra dev --extra repl
-      - name: Exercise inspection, bounded subprocesses, and transactional output
-        run: >-
-          uv run pytest -q
-          tests/test_windows_source_boundary.py
-          tests/test_tree_snapshot_limits.py
-          tests/test_project_inspect.py
-          tests/test_scaffold.py::test_scaffold_merges_autoform_rules_into_lake_gitignore
-          tests/test_scaffold.py::test_windows_cross_interface_gitignore_identity_ignores_ctime_only
-          tests/test_scaffold.py::test_scaffold_refuses_case_variants_of_managed_paths
-          tests/test_skeleton.py::test_bounded_command_rejects_excess_output
-          tests/test_skeleton.py::test_bounded_command_caps_stdout_and_stderr_together
-          tests/test_skeleton.py::test_bounded_command_rejects_invalid_utf8
-          tests/test_skeleton.py::test_bounded_command_timeout_kills_descendants
-          tests/test_skeleton.py::test_bounded_command_rejects_a_successful_parent_with_a_live_descendant
-          tests/test_skeleton.py::test_bounded_command_interruption_kills_the_process
-          tests/test_skeleton.py::test_packet_publication_rolls_back_both_trees_on_commit_failure
-          tests/test_skeleton.py::test_packet_publication_rolls_back_when_interrupted_after_backup_rename
-          tests/test_skeleton.py::test_packet_publication_restores_old_trees_when_quarantine_cleanup_fails
-          tests/test_skeleton.py::test_packet_publication_does_not_overwrite_during_backup_restore
-          tests/test_claims.py::test_git_runs_without_terminal_prompts
-          tests/test_claims.py::test_git_stops_at_the_deadline_and_names_the_step
-          tests/test_claims.py::test_git_does_not_start_once_the_deadline_has_passed
+          name: atlas-shots
+          path: screenshots
@@ -0,0 +1,59 @@
+"""Screenshot a few real ATLAS pages served on 127.0.0.1:8765 (evidence only)."""
+from pathlib import Path
+
+from playwright.sync_api import sync_playwright
+
+BASE = "http://127.0.0.1:8765"
+SHOTS = Path("screenshots")
+SHOTS.mkdir(exist_ok=True)
+PAGES = [
+    ("home", "/"),
+    ("roadmap", "/roadmap/"),
+    ("topic", "/roadmap/Algebra/"),
+    ("chapter", "/roadmap/Algebra/MathlibExt/"),
+    ("theorem", "/roadmap/Algebra/MathlibExt/#is-ladditive"),
+]
+
+
+def shoot(page, name: str, path: str, light: bool) -> None:
+    try:
+        page.goto(BASE + path, wait_until="load", timeout=90000)
+        page.wait_for_timeout(3500)
+        if light:
+            page.evaluate("document.body.setAttribute('data-md-color-scheme', 'default')")
+            page.wait_for_timeout(1200)
+        page.screenshot(path=str(SHOTS / f"{name}.png"))
+    except Exception as error:  # evidence only
+        (SHOTS / f"{name}.err.txt").write_text(repr(error)[:600], encoding="utf-8")
+
+
+with sync_playwright() as p:
+    browser = p.webkit.launch()
+    desktop = browser.new_context(viewport={"width": 1440, "height": 900})
+    page = desktop.new_page()
+    for name, path in PAGES:
+        shoot(page, f"{name}-1440-dark", path, light=False)
+        shoot(page, f"{name}-1440-light", path, light=True)
+    desktop.close()
+    phone = browser.new_context(viewport={"width": 390, "height": 844}, device_scale_factor=2, is_mobile=True, has_touch=True)
+    page = phone.new_page()
+    for name, path in PAGES:
+        shoot(page, f"{name}-390-dark", path, light=False)
+    phone.close()
+    tablet = browser.new_context(viewport={"width": 1000, "height": 800})
+    page = tablet.new_page()
+    for name, path in PAGES:
+        if name in ("roadmap", "theorem"):
+            shoot(page, f"{name}-1000-dark", path, light=False)
+    # The same chapter with one status unchecked, to show the toolbar once "Show N filtered out" appears.
+    try:
+        page.goto(BASE + "/roadmap/Algebra/MathlibExt/", wait_until="load", timeout=90000)
+        page.wait_for_timeout(3500)
+        page.locator(".bp-dag-filter-summary").click()
+        page.locator(".bp-dag-filter-popover input[type=checkbox]:checked").first.uncheck()
+        page.wait_for_timeout(1200)
+        page.screenshot(path=str(SHOTS / "filtered-1000-dark.png"))
+    except Exception as error:  # evidence only
+        (SHOTS / "filtered-1000-dark.err.txt").write_text(repr(error)[:600], encoding="utf-8")
+    tablet.close()
+    browser.close()