Repository navigation
Name every Lean tool, link skills to their exact command, and state the default debrief #2219
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 |