Mac Malone

@adamtopaz I assume you mean have mathlib have a tag/branch per supported Lean version and then have Lake fix mathlib in its template to said branch corresponding to the toolchain...

Adding an Lake option for `init`/`new` that passes the option through to the Git CLI (ala `-W` for C compilers) is a good idea and would be nice to have....

@mik-jozef > And I believe this should be the default behavior as well ,,, ignores the possibility one could use a different version control system, and is also inconsistent with...

I am shocked this matters so much as lake is still computing transitive imports for quite a few modules. I suspect that if you turned on precompiled modules or used...

> Yeah, turning on precompiled modules will still cause the quadratic behavior at the moment. But we will only use them in mathlib if we can selectively enable them for...

@gebner > Is anything missing from this PR? I did a quick review and if the two comments above are addressed, everything should be good for a merge.

@gebner > If I understand it correctly, then we only enable precompiled modules if one of the _direct_ imports is precompiled ... Did I miss something obvious? No, I think...

The fix, though, I think is simple. We just need to pass the module's transitive imports rather than the direct imports here: https://github.com/leanprover/lake/blob/84dd6d75c722f24955cefd422114c1e7f4da2d40/Lake/Build/Module.lean#L94

@gebner > In particular, we need to do something more clever than go through all transitive imports for every module (because that's quadratic). While I can see potentially ways to...

I would love to see this change! Avoiding multiple installs of the same toolchain under different names would be wonderful (and save me disk space). What will be procedure for...