mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 10:24:07 +00:00
320ddae700
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>
This is the repository for Lean 4.
About
- Quickstart
- Homepage
- Theorem Proving Tutorial
- Functional Programming in Lean
- Documentation Overview
- Language Reference
- Release notes starting at v4.0.0-m3
- Examples
- External Contribution Guidelines
Installation
See Install Lean.
Contributing
Please read our Contribution Guidelines first.
Building from Source
See Building Lean.