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
Draft
Kha wants to merge 5 commits into
base: master
Choose a base branch
from
Draft

feat: re-integrate lean4checker as leanchecker #11887

Kha wants to merge 5 commits into from

Conversation

@Kha
Copy link
Member

@Kha Kha commented Jan 3, 2026 •
edited by kim-em
Loading

This PR makes the external checker lean4checker available as the existing leanchecker binary already known to elan.

TODO:

  • re-integrate tests
  • address deprecation notice in Replay

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 <noreply@anthropic.com>
@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

Mathlib CI status (docs):

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

breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan builds-manual CI has verified that the Lean Language Reference 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 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