|
1 | 1 | name: tests |
2 | 2 |
|
3 | 3 | on: |
4 | | - # main tests each merged commit. scratch/ branches run CI on a branch with no |
5 | | - # pull request; every other branch runs through pull_request. |
6 | 4 | push: |
7 | | - branches: [main, "scratch/**"] |
8 | | - pull_request: |
| 5 | + branches: ["scratch/**"] |
9 | 6 |
|
10 | 7 | permissions: |
11 | 8 | contents: read |
12 | 9 |
|
13 | | -# A newer commit on a pull request cancels the run for the older one. Each push |
14 | | -# gets a group of its own: runs that share a group wait one at a time, and a |
15 | | -# newer one cancels any still waiting, so runs on main would skip commits. |
16 | | -concurrency: |
17 | | - group: tests-${{ github.event.pull_request.number || github.run_id }} |
18 | | - cancel-in-progress: ${{ github.event_name == 'pull_request' }} |
19 | | - |
20 | 10 | jobs: |
21 | | - test: |
22 | | - runs-on: ubuntu-latest |
23 | | - timeout-minutes: 30 |
24 | | - strategy: |
25 | | - matrix: |
26 | | - python-version: ["3.10", "3.13"] |
27 | | - steps: |
28 | | - - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 |
29 | | - - uses: actions/setup-node@249970729cb0ef3589644e2896645e5dc5ba9c38 # v6 |
30 | | - with: |
31 | | - node-version: "22.23.2" |
32 | | - - name: Install pinned explorer compiler |
33 | | - run: | |
34 | | - timeout --signal=TERM --kill-after=30s 3m npm ci --ignore-scripts --no-audit --no-fund --prefer-offline \ |
35 | | - --fetch-timeout=30000 --fetch-retries=2 --fetch-retry-mintimeout=2000 --fetch-retry-maxtimeout=10000 |
36 | | - - run: npm run check:explorer |
37 | | - - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0 |
38 | | - with: |
39 | | - version: "0.12.1" |
40 | | - python-version: ${{ matrix.python-version }} |
41 | | - enable-cache: true |
42 | | - - run: uv sync --locked --extra dev --extra repl |
43 | | - - run: uv run ruff check autoform_cli servers tests |
44 | | - - run: uv run pytest -q |
45 | | - - run: make check-example |
46 | | - |
47 | 11 | browser: |
48 | | - name: WebKit integrated book and explorer regressions |
| 12 | + name: WebKit selected tests |
49 | 13 | runs-on: ubuntu-latest |
50 | 14 | timeout-minutes: 25 |
51 | | - # Playwright's image for the pinned playwright==1.62.0 carries WebKit and its |
52 | | - # system libraries, so the job does not fetch them from an Ubuntu mirror; |
53 | | - # that apt step alone has taken over 8 minutes and timed the job out. |
54 | | - container: |
55 | | - image: mcr.microsoft.com/playwright/python:v1.62.0-noble@sha256:aa81288e738725378becba5b3e06cb0f3a7f012a610e87e8d767a090ea3f740d |
56 | | - # In a container, run steps default to sh; keep bash, as on the host jobs. |
57 | | - defaults: |
58 | | - run: |
59 | | - shell: bash |
60 | 15 | steps: |
61 | 16 | - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 |
62 | 17 | - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0 |
63 | 18 | with: |
64 | 19 | version: "0.12.1" |
65 | 20 | python-version: "3.13" |
66 | 21 | enable-cache: true |
67 | | - - name: Install locked browser test environment |
68 | | - run: uv sync --frozen --extra dev --extra browser |
69 | | - # The explorer's typesetting runs the real MathJax, served in place of |
70 | | - # the CDN from the same checked tarball as the MathJax job's. |
71 | | - - name: Install pinned MathJax 3.2.2 |
72 | | - run: | |
73 | | - set -euo pipefail |
74 | | - timeout --signal=TERM --kill-after=15s 2m curl -sSfL \ |
75 | | - https://registry.npmjs.org/mathjax/-/mathjax-3.2.2.tgz -o mathjax.tgz |
76 | | - echo "1b9c0a1c44df864e915690558e72adb9cc5203360daefd385084ced3b6c64c09 mathjax.tgz" \ |
77 | | - | sha256sum --check --strict |
78 | | - mkdir mathjax |
79 | | - tar xzf mathjax.tgz -C mathjax |
80 | | - echo "AUTOFORM_MATHJAX_DIR=$PWD/mathjax/package" >> "$GITHUB_ENV" |
81 | | - echo "AUTOFORM_MATHJAX_ES5=$PWD/mathjax/package/es5" >> "$GITHUB_ENV" |
82 | | - - name: Run integrated book, explorer and genuine MathJax regressions |
83 | | - run: >- |
84 | | - uv run --frozen --extra dev --extra browser pytest -q |
85 | | - tests/test_dag_viewer_browser.py tests/test_integrated_explorer_browser.py |
86 | | - tests/test_integrated_workspace_browser.py tests/test_integrated_continuity_browser.py |
87 | | - tests/test_scoped_overview_browser.py |
| 22 | + - run: uv sync --frozen --extra dev --extra browser |
| 23 | + - run: uv run --frozen --extra browser playwright install --with-deps webkit |
| 24 | + - run: uv run --frozen --extra dev --extra browser pytest -q tests/test_scoped_overview_browser.py |
88 | 25 | env: |
89 | 26 | AUTOFORM_REQUIRE_BROWSER_TESTS: "1" |
90 | | - AUTOFORM_REQUIRE_MATHJAX_TESTS: "1" |
91 | | - AUTOFORM_UI_SCREENSHOT_DIR: ${{ runner.temp }}/autoform-ui-evidence |
92 | | - - name: Preserve browser UI screenshots and diagnostics |
93 | | - if: always() |
94 | | - uses: actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9 # v7 |
95 | | - with: |
96 | | - name: integrated-ui-evidence-${{ github.run_id }} |
97 | | - path: ${{ runner.temp }}/autoform-ui-evidence |
98 | | - if-no-files-found: warn |
99 | | - retention-days: 7 |
100 | | - |
101 | | - mathjax: |
102 | | - name: MathJax read-back cards (Node) |
103 | | - runs-on: ubuntu-latest |
104 | | - timeout-minutes: 15 |
105 | | - steps: |
106 | | - - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 |
107 | | - - uses: actions/setup-node@249970729cb0ef3589644e2896645e5dc5ba9c38 # v6 |
108 | | - with: |
109 | | - node-version: "22.23.2" |
110 | | - - name: Install locked native DOM test bridge |
111 | | - run: | |
112 | | - timeout --signal=TERM --kill-after=30s 3m npm ci --ignore-scripts --no-audit --no-fund --prefer-offline \ |
113 | | - --fetch-timeout=30000 --fetch-retries=2 --fetch-retry-mintimeout=2000 --fetch-retry-maxtimeout=10000 |
114 | | - - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0 |
115 | | - with: |
116 | | - version: "0.12.1" |
117 | | - python-version: "3.13" |
118 | | - enable-cache: true |
119 | | - - name: Install locked development environment |
120 | | - run: uv sync --frozen --extra dev |
121 | | - # The npm tarball of the release the site loads, checked against the |
122 | | - # sha256 of the one whose sha1 and sha512 npm publishes. |
123 | | - - name: Install pinned MathJax 3.2.2 |
124 | | - run: | |
125 | | - set -euo pipefail |
126 | | - timeout --signal=TERM --kill-after=15s 2m curl -sSfL \ |
127 | | - https://registry.npmjs.org/mathjax/-/mathjax-3.2.2.tgz -o mathjax.tgz |
128 | | - echo "1b9c0a1c44df864e915690558e72adb9cc5203360daefd385084ced3b6c64c09 mathjax.tgz" \ |
129 | | - | sha256sum --check --strict |
130 | | - mkdir mathjax |
131 | | - tar xzf mathjax.tgz -C mathjax |
132 | | - echo "AUTOFORM_MATHJAX_DIR=$PWD/mathjax/package" >> "$GITHUB_ENV" |
133 | | - - name: Typeset read-back cards in Node with the script render writes |
134 | | - run: uv run --frozen --extra dev pytest -q tests/test_site_mathjax_node.py |
135 | | - env: |
136 | | - AUTOFORM_REQUIRE_MATHJAX_TESTS: "1" |
137 | | - |
138 | | - real-lean: |
139 | | - name: real Lean (fixture toolchain) |
140 | | - runs-on: ubuntu-latest |
141 | | - timeout-minutes: 75 |
142 | | - steps: |
143 | | - - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 |
144 | | - - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0 |
145 | | - with: |
146 | | - version: "0.12.1" |
147 | | - python-version: "3.13" |
148 | | - enable-cache: true |
149 | | - - name: Install locked development environment |
150 | | - run: timeout --signal=TERM --kill-after=30s 3m uv sync --frozen --extra dev --extra repl |
151 | | - - name: Install pinned Elan |
152 | | - run: | |
153 | | - set -euo pipefail |
154 | | - timeout --signal=TERM --kill-after=15s 2m curl -sSfL \ |
155 | | - https://github.com/leanprover/elan/releases/download/v4.2.3/elan-x86_64-unknown-linux-gnu.tar.gz \ |
156 | | - -o elan.tar.gz |
157 | | - echo "df0b2b3a439961ffcbb3985214365ffe40f49bc871df04dff268c7d8e21ca8b2 elan.tar.gz" \ |
158 | | - | sha256sum --check --strict |
159 | | - tar xzf elan.tar.gz |
160 | | - ./elan-init -y --default-toolchain none |
161 | | - echo "$HOME/.elan/bin" >> "$GITHUB_PATH" |
162 | | - - name: Install the fixture's Lean toolchain |
163 | | - run: | |
164 | | - set -euo pipefail |
165 | | - timeout --signal=TERM --kill-after=30s 10m \ |
166 | | - elan toolchain install "$(tr -d '\r\n' < tests/fixtures/skeleton-project/lean-toolchain)" |
167 | | - command -v lake |
168 | | - - name: Install the library fixture's Lean toolchain |
169 | | - run: | |
170 | | - set -euo pipefail |
171 | | - timeout --signal=TERM --kill-after=30s 10m \ |
172 | | - elan toolchain install "$(tr -d '\r\n' < tests/fixtures/library-project/lean-toolchain)" |
173 | | - - name: Build a project from the bundled creation release |
174 | | - run: | |
175 | | - set -euo pipefail |
176 | | - generated_project="$RUNNER_TEMP/autoform-created-project" |
177 | | - uv run autoform project new "$generated_project" \ |
178 | | - --package GeneratedProject \ |
179 | | - --release lean-v4.32.2-mathlib-v4.32.2 |
180 | | - cd "$generated_project" |
181 | | - timeout --signal=TERM --kill-after=30s 20m lake exe cache get |
182 | | - timeout --signal=TERM --kill-after=30s 10m lake build |
183 | | - - name: Audit the created project as its workflow does |
184 | | - run: | |
185 | | - set -euo pipefail |
186 | | - # The template's helper, so the step audits this checkout's probe on a |
187 | | - # build that imports all of Mathlib. |
188 | | - helper="$PWD/autoform_cli/templates/github/autoform_audit.py" |
189 | | - archive="$RUNNER_TEMP/autoform-created-root.tgz" |
190 | | - probe="$RUNNER_TEMP/autoform-created-probe.lean" |
191 | | - output="$RUNNER_TEMP/autoform-created-probe.out" |
192 | | - cd "$RUNNER_TEMP/autoform-created-project" |
193 | | - lake pack "$archive" |
194 | | - python3 "$helper" GeneratedProject "$archive" "$probe" |
195 | | - lean_path="$(lake env printenv LEAN_PATH)" |
196 | | - AUTOFORM_AUDIT_LEAN_PATH="$lean_path" LEAN_ABORT_ON_PANIC=1 \ |
197 | | - timeout --signal=TERM --kill-after=30s 15m lean "$probe" | tee "$output" |
198 | | - if ! tail -n 1 "$output" | grep -Eq '^kernel trust clean \('; then |
199 | | - echo "the audit probe did not end with its success line" >&2 |
200 | | - exit 1 |
201 | | - fi |
202 | | - - name: Run the impact probe against real Lean |
203 | | - run: timeout --signal=TERM --kill-after=30s 10m uv run pytest -q tests/test_impact.py |
204 | | - env: |
205 | | - AUTOFORM_REQUIRE_REAL_LEAN_TESTS: "1" |
206 | | - - name: Run the library index generator against real Lean |
207 | | - run: timeout --signal=TERM --kill-after=30s 30m uv run pytest -q tests/test_library_generate.py |
208 | | - env: |
209 | | - AUTOFORM_REQUIRE_REAL_LIBRARY_TESTS: "1" |
210 | | - - name: Run the open-statement audit and contract against real Lean |
211 | | - run: timeout --signal=TERM --kill-after=30s 10m uv run pytest -q tests/test_lake_artifact_audit.py tests/test_contract.py |
212 | | - env: |
213 | | - AUTOFORM_REQUIRE_REAL_LEAN_TESTS: "1" |
214 | | - - name: Run the LSP lifecycle and diagnostics checks against real Lean |
215 | | - run: >- |
216 | | - timeout --signal=TERM --kill-after=30s 10m uv run pytest -q -k real_lean |
217 | | - tests/test_lsp_protocol.py tests/test_batch_diagnostics.py |
218 | | - env: |
219 | | - AUTOFORM_REQUIRE_REAL_LEAN_TESTS: "1" |
220 | | - AUTOFORM_REAL_LEAN_MATHLIB_PROJECT: ${{ runner.temp }}/autoform-created-project |
221 | | - |
222 | | - real-lean-skeleton: |
223 | | - name: real Lean skeleton suite (fixture toolchain) |
224 | | - runs-on: ubuntu-latest |
225 | | - timeout-minutes: 40 |
226 | | - steps: |
227 | | - - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 |
228 | | - - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0 |
229 | | - with: |
230 | | - version: "0.12.1" |
231 | | - python-version: "3.13" |
232 | | - enable-cache: true |
233 | | - - name: Install locked development environment |
234 | | - run: timeout --signal=TERM --kill-after=30s 3m uv sync --frozen --extra dev --extra repl |
235 | | - - name: Install pinned Elan |
236 | | - run: | |
237 | | - set -euo pipefail |
238 | | - timeout --signal=TERM --kill-after=15s 2m curl -sSfL \ |
239 | | - https://github.com/leanprover/elan/releases/download/v4.2.3/elan-x86_64-unknown-linux-gnu.tar.gz \ |
240 | | - -o elan.tar.gz |
241 | | - echo "df0b2b3a439961ffcbb3985214365ffe40f49bc871df04dff268c7d8e21ca8b2 elan.tar.gz" \ |
242 | | - | sha256sum --check --strict |
243 | | - tar xzf elan.tar.gz |
244 | | - ./elan-init -y --default-toolchain none |
245 | | - echo "$HOME/.elan/bin" >> "$GITHUB_PATH" |
246 | | - - name: Install the fixture's Lean toolchain |
247 | | - run: | |
248 | | - set -euo pipefail |
249 | | - timeout --signal=TERM --kill-after=30s 10m \ |
250 | | - elan toolchain install "$(tr -d '\r\n' < tests/fixtures/skeleton-project/lean-toolchain)" |
251 | | - command -v lake |
252 | | - - name: Run the skeleton suite against real Lean |
253 | | - run: >- |
254 | | - timeout --signal=TERM --kill-after=30s 35m uv run pytest -q |
255 | | - tests/test_skeleton.py |
256 | | - tests/test_project_inspect.py::test_stale_inherited_mathlib_is_ignored_by_real_lake |
257 | | - env: |
258 | | - AUTOFORM_REQUIRE_REAL_LEAN_TESTS: "1" |
259 | | - |
260 | | - real-repl: |
261 | | - name: real REPL (fixture toolchain) |
262 | | - runs-on: ubuntu-latest |
263 | | - timeout-minutes: 15 |
264 | | - steps: |
265 | | - - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 |
266 | | - - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0 |
267 | | - with: |
268 | | - version: "0.12.1" |
269 | | - python-version: "3.13" |
270 | | - enable-cache: true |
271 | | - - name: Install pinned Elan |
272 | | - run: | |
273 | | - set -euo pipefail |
274 | | - timeout --signal=TERM --kill-after=15s 2m curl -sSfL \ |
275 | | - https://github.com/leanprover/elan/releases/download/v4.2.3/elan-x86_64-unknown-linux-gnu.tar.gz \ |
276 | | - -o elan.tar.gz |
277 | | - echo "df0b2b3a439961ffcbb3985214365ffe40f49bc871df04dff268c7d8e21ca8b2 elan.tar.gz" \ |
278 | | - | sha256sum --check --strict |
279 | | - tar xzf elan.tar.gz |
280 | | - ./elan-init -y --default-toolchain none |
281 | | - echo "$HOME/.elan/bin" >> "$GITHUB_PATH" |
282 | | - - name: Build the REPL fixture |
283 | | - working-directory: tests/fixtures/repl-smoke |
284 | | - run: | |
285 | | - set -euo pipefail |
286 | | - timeout --signal=TERM --kill-after=30s 5m \ |
287 | | - elan toolchain install "$(tr -d '\r\n' < lean-toolchain)" |
288 | | - timeout --signal=TERM --kill-after=30s 8m lake build Mathlib Secret @repl/repl |
289 | | - - name: Install the minimum supported Lean toolchain |
290 | | - run: | |
291 | | - set -euo pipefail |
292 | | - timeout --signal=TERM --kill-after=30s 5m \ |
293 | | - elan toolchain install "$(tr -d '\r\n' < tests/fixtures/minimum-lean/lean-toolchain)" |
294 | | - - name: Install locked development environment |
295 | | - run: timeout --signal=TERM --kill-after=30s 3m uv sync --frozen --extra dev --extra repl |
296 | | - - name: Run the REPL suite against the pinned upstream REPL |
297 | | - run: timeout --signal=TERM --kill-after=30s 10m uv run pytest -q tests/test_real_repl.py |
298 | | - env: |
299 | | - AUTOFORM_RUN_REAL_REPL_TESTS: "1" |
300 | | - |
301 | | - windows-hardening: |
302 | | - name: Windows inspection, subprocess, and publication hardening |
303 | | - runs-on: windows-latest |
304 | | - timeout-minutes: 15 |
305 | | - steps: |
306 | | - - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 |
307 | | - - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0 |
308 | | - with: |
309 | | - version: "0.12.1" |
310 | | - python-version: "3.13" |
311 | | - enable-cache: true |
312 | | - - run: uv sync --frozen --extra dev --extra repl |
313 | | - - name: Exercise inspection, bounded subprocesses, and transactional output |
314 | | - run: >- |
315 | | - uv run pytest -q |
316 | | - tests/test_windows_source_boundary.py |
317 | | - tests/test_tree_snapshot_limits.py |
318 | | - tests/test_project_inspect.py |
319 | | - tests/test_scaffold.py::test_scaffold_merges_autoform_rules_into_lake_gitignore |
320 | | - tests/test_scaffold.py::test_windows_cross_interface_gitignore_identity_ignores_ctime_only |
321 | | - tests/test_scaffold.py::test_scaffold_refuses_case_variants_of_managed_paths |
322 | | - tests/test_skeleton.py::test_bounded_command_rejects_excess_output |
323 | | - tests/test_skeleton.py::test_bounded_command_caps_stdout_and_stderr_together |
324 | | - tests/test_skeleton.py::test_bounded_command_rejects_invalid_utf8 |
325 | | - tests/test_skeleton.py::test_bounded_command_timeout_kills_descendants |
326 | | - tests/test_skeleton.py::test_bounded_command_rejects_a_successful_parent_with_a_live_descendant |
327 | | - tests/test_skeleton.py::test_bounded_command_interruption_kills_the_process |
328 | | - tests/test_skeleton.py::test_packet_publication_rolls_back_both_trees_on_commit_failure |
329 | | - tests/test_skeleton.py::test_packet_publication_rolls_back_when_interrupted_after_backup_rename |
330 | | - tests/test_skeleton.py::test_packet_publication_restores_old_trees_when_quarantine_cleanup_fails |
331 | | - tests/test_skeleton.py::test_packet_publication_does_not_overwrite_during_backup_restore |
332 | | - tests/test_claims.py::test_git_runs_without_terminal_prompts |
333 | | - tests/test_claims.py::test_git_stops_at_the_deadline_and_names_the_step |
334 | | - tests/test_claims.py::test_git_does_not_start_once_the_deadline_has_passed |
0 commit comments