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.