lean4

mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 10:24:07 +00:00

Files

Kim Morrison 320ddae700 feat: add lake-ci label to enable full Lake test suite (#12836 )

This PR adds a `lake-ci` label that enables the full Lake test suite in
CI,
avoiding the need to temporarily commit and revert changes to
`tests/CMakeLists.txt`. The `lake-ci` label implies `release-ci` (check
level
3), so all release platforms are also tested.

Motivated by
https://github.com/leanprover/lean4/pull/12540#issuecomment-4000081071
where @tydeu requested running `release-ci` with Lake tests enabled,
which
previously required temporarily uncommenting a line in
`tests/CMakeLists.txt`.

Users can add it via a PR comment containing `lake-ci` on its own line,
or by
adding the label manually. CI automatically restarts when the label is
added.

Implementation:
- `ci.yml`: detect `lake-ci` label, set check level 3, pass
`-DLAKE_CI=ON` to cmake
- `tests/CMakeLists.txt`: `option(LAKE_CI ...)` conditionally enables
full `tests/lake/tests/` glob
- `restart-on-label.yml`: restart CI on `lake-ci` label
- `labels-from-comments.yml`: support `lake-ci` comment

🤖 Prepared with Claude Code

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

2026-03-10 03:23:35 +00:00

actionlint.yml

chore: CI: bump actions/checkout from 5 to 6 (#11459 )

2026-01-09 07:43:13 +00:00

awaiting-manual.yml

fix: use pull_request_target for label-triggered workflows (#12638 )

2026-03-01 19:20:56 +11:00

awaiting-mathlib.yml

fix: use pull_request_target for label-triggered workflows (#12638 )

2026-03-01 19:20:56 +11:00

backport.yml

chore: CI: add backport action