Skip to content

feat: re-integrate lean4checker as leanchecker #11887

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
Kha merged 14 commits into from
Jan 8, 2026
Merged

feat: re-integrate lean4checker as leanchecker #11887

Kha merged 14 commits into from
Jan 8, 2026

Conversation

@Kha
Copy link
Member

@Kha Kha commented Jan 3, 2026 •
edited
Loading

This PR makes the external checker lean4checker available as the existing leanchecker binary already known to elan, allowing for out-of-the-box access to it.

kim-em and others added 2 commits January 5, 2026 13:20
@kim-em @claude
fix: add LeanChecker build rule for non-Lake builds
848ee1f 
This PR adds the missing leanmake rule for building libLeanChecker.a
when USE_LAKE=OFF. The secondary CI builds (Linux release and macOS
aarch64) use this mode and were failing because the leanchecker binary
target expected libLeanChecker.a to exist but there was no rule to
build it.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude Opus 4.5 <[email protected]>
@kim-em
drop old Replay
7ba979c
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jan 5, 2026
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 5, 2026
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#11887
e081fc1
@github-actions github-actions bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Jan 5, 2026
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jan 5, 2026
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#11887
c6fa8d6
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Jan 5, 2026
@leanprover-bot
Update lean-toolchain for testing leanprover/lean4#11887
8e6aebc
@leanprover-bot leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Jan 5, 2026
@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Jan 5, 2026 •
edited
Loading

Reference manual CI status:

@leanprover-community-bot leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Jan 5, 2026
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Jan 5, 2026 •
edited
Loading

Mathlib CI status (docs):

kim-em and others added 3 commits January 6, 2026 11:28
@kim-em @claude
test: add leanchecker tests
d6d3839 
This PR adds tests for the `leanchecker` binary, ported from the
lean4checker repository. Tests include:

- Environment hacking detection (AddFalse, AddFalseConstructor, ReplaceAxiom)
- Private import conflict detection in --fresh mode (PrivateConflictC)
- Quot/Eq dependency ordering (QuotEq)

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude Opus 4.5 <[email protected]>
@kim-em
test: INTENTIONALLY BREAK test to verify CI catches it
7ed7593
@kim-em
test: restore correct expected output (CI caught the intentional break)
d25b36f
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 6, 2026
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#11887
7895ea1
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jan 6, 2026
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#11887
bbafa94
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Jan 6, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#11887
febef88
@Kha Kha added the release-ci Enable all CI checks for a PR, like is done for releases label Jan 7, 2026
@Kha Kha marked this pull request as ready for review January 7, 2026 15:26
@Kha Kha enabled auto-merge January 7, 2026 15:26
Kha
Kha commented Jan 7, 2026
View reviewed changes
src/LeanChecker.lean
for path in (← SearchPath.findAllWithExt sp "olean") do
if let some m := (← searchModuleNameOfFileName path sp) then
if target.isPrefixOf m then
if !fresh && target.isPrefixOf m || target == m then
Copy link
Member Author

@Kha Kha Jan 7, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@digama0 Note this fix in --fresh's behavior

@Kha Kha removed the release-ci Enable all CI checks for a PR, like is done for releases label Jan 8, 2026
@Kha Kha added the merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. label Jan 8, 2026
@Kha Kha added this pull request to the merge queue Jan 8, 2026
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 8, 2026
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#11887
5c592cd
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jan 8, 2026
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#11887
50397f1
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Jan 8, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#11887
527bbaa
Merged via the queue into leanprover:master with commit 1361d73 Jan 8, 2026
19 checks passed
@leanprover-community-bot leanprover-community-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Jan 8, 2026
@Kha Kha deleted the push-pwzqrnlnynxz branch January 8, 2026 11:00
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

builds-manual CI has verified that the Lean Language Reference builds against this PR builds-mathlib CI has verified that Mathlib builds against this PR changelog-other mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@Kha @leanprover-bot @leanprover-community-bot @kim-em