chore: upstream shake from Mathlib to Batteries

[Vierkantor]

trafficstars

The shake command doesn't depend on Mathlib so let's upstream it and make it available for other projects.

This version still has some settings hardcoded to use Mathlib as default. In #1205 I change this to use Lake's default targets instead.

Mathlib adaptation PR: https://github.com/leanprover-community/mathlib4/pull/23916

Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Spinning.20off.20.60mathlib-linters.60.20and.20.60shake.60.20repo

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch batteries-pr-testing-1204 has successfully built against this PR. (2025-04-10 12:58:47) View Log
• ✅ Mathlib branch batteries-pr-testing-1204 has successfully built against this PR. (2025-04-10 16:09:00) View Log

[Vierkantor]

I have tested that shake does sensible things, and indeed it reports quite a few files in Batteries can be shaken! The default target to run shake on is still Mathlib, currently working on making Lake tell me the default target instead. But I think we can leave that to a follow-up PR.

[grunweg]

Sure, I agree. Can you add the default target bit to the PR description? (I cannot.)

[fgdorais]

What is the status of this PR?

[bryangingechen]

It looks to me like the discussion on Zulip about whether shake should be in its own repository is still unresolved.