tests.yml

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:

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: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0
        with:
          version: "0.12.1"
          python-version: ${{ matrix.python-version }}
          enable-cache: true
      - run: uv sync --locked --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 dependency explorer regressions
    runs-on: ubuntu-latest
    timeout-minutes: 15
    # Playwright's image for the pinned playwright==1.62.0 carries WebKit and its
    # system libraries, so the job does not fetch them from an Ubuntu mirror;
    # that apt step alone has taken over 8 minutes and timed the job out.
    container:
      image: mcr.microsoft.com/playwright/python:v1.62.0-noble@sha256:aa81288e738725378becba5b3e06cb0f3a7f012a610e87e8d767a090ea3f740d
    # In a container, run steps default to sh; keep bash, as on the host jobs.
    defaults:
      run:
        shell: bash
    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
      # The explorer's typesetting runs the real MathJax, served in place of
      # the CDN from the same checked tarball as the MathJax job's.
      - 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: Run dependency explorer browser regressions
        run: uv run --frozen --extra dev --extra browser pytest -q tests/test_dag_viewer_browser.py
        env:
          AUTOFORM_REQUIRE_BROWSER_TESTS: "1"
          AUTOFORM_REQUIRE_MATHJAX_TESTS: "1"

  mathjax:
    name: MathJax read-back cards (Node)
    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 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