Commit 2024-05-29 17:17 1ea200b2

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

Modified lakefile.lean

Created scripts/mk_all.lean

added def getAll

added def getLeanLibs

added def main

added def mkAll

added def mkAllCLI