Skip to content

feat: add lake shake command #11921

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

feat: add lake shake command #11921

kim-em wants to merge 9 commits into from

Conversation

@kim-em
Copy link
Collaborator

@kim-em kim-em commented Jan 7, 2026

This PR adds lake shake as a built-in Lake command, moving the shake functionality from script/Shake.lean into the Lake CLI.

Motivation

Per discussion with @Kha and @tydeu, having shake as a top-level Lake command is preferable to lake exe shake because:

  • Avoids the awkwardness of accessing core tools via lake exe
  • Compiles shake into the Lake binary, avoiding lakefile issues
  • No benefit to lazy compilation on user machines for this tool

Changes

  • Move shake logic from script/Shake.lean to src/lake/Lake/CLI/Shake.lean
  • Add lake shake command dispatch in Lake/CLI/Main.lean
  • Add help text in Lake/CLI/Help.lean
  • Remove the standalone shake executable from script/lakefile.toml

Usage

lake shake [OPTIONS] [<MODULE>...]

See lake shake --help for full documentation.

🤖 Prepared with Claude Code

@kim-em kim-em requested a review from tydeu as a code owner January 7, 2026 01:30
@kim-em kim-em added changelog-language Language features and metaprograms changelog-lake Lake and removed changelog-language Language features and metaprograms labels Jan 7, 2026
@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 7, 2026
@leanprover-community-bot
Copy link
Collaborator

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

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 11e4e44be070ec99bc734e40f8431fd92725842d --onto 0f866236c7c2e77e8d12ff61d08ef48694a0cbfb. You can force Mathlib CI using the force-mathlib-ci label. (2026-01-07 03:09:23)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 11e4e44be070ec99bc734e40f8431fd92725842d --onto ff87bcb8e57caeee38aa1dd05a212c0b2c51a902. You can force Mathlib CI using the force-mathlib-ci label. (2026-01-07 18:35:17)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7d5a96941e5b92d2f5956f7adf078dfc253bf4ba --onto 0ad15fe98273448cff34de5b777550a82e09f5f9. You can force Mathlib CI using the force-mathlib-ci label. (2026-01-09 07:21:40)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Jan 7, 2026 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 11e4e44be070ec99bc734e40f8431fd92725842d --onto 0f866236c7c2e77e8d12ff61d08ef48694a0cbfb. You can force reference manual CI using the force-manual-ci label. (2026-01-07 03:09:25)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 11e4e44be070ec99bc734e40f8431fd92725842d --onto ff87bcb8e57caeee38aa1dd05a212c0b2c51a902. You can force reference manual CI using the force-manual-ci label. (2026-01-07 18:35:19)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 7d5a96941e5b92d2f5956f7adf078dfc253bf4ba --onto 0ad15fe98273448cff34de5b777550a82e09f5f9. You can force reference manual CI using the force-manual-ci label. (2026-01-09 07:21:42)

Kha
Kha requested changes Jan 7, 2026
View reviewed changes
@tydeu tydeu marked this pull request as draft January 7, 2026 21:38
kim-em and others added 8 commits January 9, 2026 05:48
@kim-em @claude @tydeu
feat: add lake shake command
e6e4751 
This PR adds `lake shake` as a built-in Lake command, moving the shake
functionality from `script/Shake.lean` into the Lake CLI. This makes the
import minimization tool available directly via `lake shake` rather than
requiring `lake exe shake` from the lean4 script directory.

The shake tool analyzes `.olean` files to detect unused imports and can
automatically fix them with `--fix`.

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

Co-Authored-By: Claude <[email protected]>
@kim-em @tydeu
fix: add missing prelude to Lake/CLI/Shake.lean
48bcb69
@kim-em @claude @tydeu
refactor: integrate shake options into Lake CLI properly
3e02f53 
- Add shake options to LakeOptions structure
- Add shake option parsing to lakeLongOption
- Update Shake.run to accept workspace search paths
- Add basic test for lake shake command

Co-Authored-By: Mac Malone <[email protected]>

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

Co-Authored-By: Claude Opus 4.5 <[email protected]>
@kim-em @claude @tydeu
fix: compare imports by module name in --fix mode
09018fb 
The import comparison in --fix mode was using full Import equality,
which includes the isExported field. This caused mismatches between
imports from olean analysis (which may have isExported=true) and
imports parsed from source files (which have isExported=false for
regular imports).

Now we compare only by module name and isMeta flag, ignoring isExported.

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

Co-Authored-By: Claude Opus 4.5 <[email protected]>
@kim-em @claude @tydeu
test: add --fix mode verification to shake test
b8e8214 
Verify that lake shake --fix actually modifies the file to match expected output.

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

Co-Authored-By: Claude Opus 4.5 <[email protected]>
@tydeu
refactor: streamline shake option processing
350622c
@tydeu
chore: enable Lake tests for PR
c039cca
@tydeu
feat: perform olean check within same lake process
f2f2291
tydeu
tydeu approved these changes Jan 9, 2026
View reviewed changes
Copy link
Member

@tydeu tydeu left a comment •
edited
Loading

Choose a reason for hiding this comment

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

For my part, I have reviewed the Lake side of this code and made few changes to make the two more closely integrated. I am happy to see this merged whenever you and Sebastian deem it ready.

I left the PR as draft because c039cca should be reverted before merging (once we are happy with the tests and they have passed a round of CI).

@kim-em
refactor: address review feedback on lake shake
2d20c52 
- Remove unused Shake.run function, rename run' to run
- Revert special-casing for isExported comparison in --fix mode
- Remove unnecessary --force flags from test
- Use relative path in test check_diff
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@Kha Kha Kha requested changes

@tydeu tydeu tydeu approved these changes

Assignees

No one assigned

Labels

changelog-lake Lake 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.

6 participants

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