Commit 2024-05-29 17:17 1ea200b2

View on Github →

feat: lake exe mk_all as a Lean executable (#11853) Running

lake exe mk_all --git

should have the same effect as running

./script/mk_all.sh

that is, it creates the files Mathlib.lean, Mathlib/Tactic.lean, Archive.lean, Counterexamples.lean. It does not create analogous files for Cache and LongestPole.

lake exe mk_all

is similar, but uses all the .lean files in Mathlib, not just the Git-managed ones. See #11874 for using the script in CI.

Estimated changes

added def getAll
added def getLeanLibs
added def main
added def mkAll
added def mkAllCLI