leanprover-community
feat: Shake autodetects which module(s) to shake
There were still a few references to Mathlib in Shake, in particular it had Mathlib hardcoded as the default module to shake. Instead ask Lake what the default targets are.
(Also remove a reference to Mathlib from the help text. We still have Mathlib as an example usage, which I think is innocent enough and can stay.)
Depends on: #1204
Mathlib CI status (docs):
- ✅ Mathlib branch batteries-pr-testing-1205 has successfully built against this PR. (2025-04-10 14:23:48) View Log
My understanding is that the equivalent PR has landed in mathlib, so this PR can be closed. (If shake were to be upstreamed to batteries, #1204 should be updated.) That said, my reading of the zulip discussion was also that moving shake to batteries had no consensus, and a separate repository might be better.
