Using shake in new projects

Stream: general

[Alexandre Rademaker]

Hi @Kim Morrison , how to use https://github.com/leanprover/lean4/blob/master/script/Shake.lean ? @Sebastian Ullrich mentioned the tool in his talk, but I didn't understand how to 'add' this script in a project. I downloaded the file, added

[[lean_exe]]
name = "shake"
root = "Shake"
supportInterpreter = true

in my lakefile.toml but I am getting a lot of errors

% lake exe shake
✖ [2/4] Building Shake
trace: .> LEAN_PATH=/Users/ar/r/bignum/.lake/packages/Cli/.lake/build/lib/lean:/Users/ar/r/bignum/.lake/packages/batteries/.lake/build/lib/lean:/Users/ar/r/bignum/.lake/packages/Qq/.lake/build/lib/lean:/Users/ar/r/bignum/.lake/packages/aesop/.lake/build/lib/lean:/Users/ar/r/bignum/.lake/packages/proofwidgets/.lake/build/lib/lean:/Users/ar/r/bignum/.lake/packages/importGraph/.lake/build/lib/lean:/Users/ar/r/bignum/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/Users/ar/r/bignum/.lake/packages/plausible/.lake/build/lib/lean:/Users/ar/r/bignum/.lake/packages/mathlib/.lake/build/lib/lean:/Users/ar/r/bignum/.lake/build/lib/lean /Users/ar/.elan/toolchains/leanprover--lean4---v4.26.0-rc2/bin/lean /Users/ar/r/bignum/Shake.lean -o /Users/ar/r/bignum/.lake/build/lib/lean/Shake.olean -i /Users/ar/r/bignum/.lake/build/lib/lean/Shake.ilean -c /Users/ar/r/bignum/.lake/build/ir/Shake.c --setup /Users/ar/r/bignum/.lake/build/ir/Shake.setup.json --json
error: Shake.lean:334:27: Unknown identifier `indirectModUseExt.getState`
warning: Shake.lean:411:39: `String.Pos` has been deprecated: Use `String.Pos.Raw` instead

[Chris Henson]

We have shake running in CI already.

[Chris Henson]

I recently added description at the bottom of CONTRIBUTING.md, it is just run via lake exe shake.

[Alexandre Rademaker]

I got it @Chris Henson , I am asking about how to make it run in a fresh project... It seems the Shake.lean file I mentioned is different from the one in the Batteries (batteries/Shake/Main.lean).

[Chris Henson]

I assumed this was a CSLib question given the channel.

[Chris Henson]

My advice would be to add batteries as a dependency and run lake exe shake as usual.

[Chris Henson]

(assuming it is not available by default)

[Alexandre Rademaker]

Yes, you are right. My fault for reusing the thread. Thank you for the advice.

[Notification Bot]

8 messages were moved here from #CSLib > Upcoming closure results for regular languages in mathlib by Kim Morrison.

[Alexandre Rademaker]

Reporting what I understood. @Sebastian Ullrich mentioned the latest version of Shake in his talk at https://sites.google.com/view/lean-at-googl-2025/. The file is here.

But apparently, another old version of Shake already exists in Batteries! Any project that imports Batteries already has the command below available.

lake exe shake

To use this latest version, I downloaded it and saved it at the root of my project. Then I added to lakefile.toml:

[[lean_exe]]
name = "sh"
root = "Shake"

I used the namesh, so that Lake executes this file and not ./.lake/packages/batteries/Shake/Main.lean. Does it make sense?

[Sebastian Ullrich]

If it works, sure. And then we'll figure out the rest when packaging it for Mathlib.