mathlib

fc0c0258 - refactor(scripts/mk_all): generate a single deterministic all.lean file (#2673)

refactor(scripts/mk_all): generate a single deterministic all.lean file (#2673) The current `mk_all.sh` script is non-deterministic, and creates invalid Lean code for the `data.matrix.notation` import. The generated `all.lean` files are also slow: they take two minutes to compile on my machine. The new script fixes all of that. The single generated `all.lean` file takes only 27 seconds to compile now.