@@ -1,51 +1,15 @@
 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
+    name: WebKit selected tests
     runs-on: ubuntu-latest
     timeout-minutes: 25
     steps:
@@ -55,258 +19,9 @@ jobs:
           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 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
+      - run: uv sync --frozen --extra dev --extra browser
+      - run: uv run --frozen --extra browser playwright install --with-deps webkit
+      - 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
-        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