Mac Malone

@Vtec234 > I don't understand what a "pre-build" or "post-build" dependency is and how I could use them to do this. Ah, I was suggesting new features, not ones present...

> And starting with the second lakefile (i.e. all the dependencies) the mmap-optimization no longer works, Isn't that a bug with Lean then?

> The bigger issue is that we're compiling multiple lakefiles at all, since importing alone (excluding olean loading time) costs around 130ms per lakefile. How do you propose fixing this?...

Thanks for all the suggestions! > _Reduce imports._ ]..] This is [easy to try out](https://github.com/gebner/lake/commit/91f498118c4cffe496716bcce0aa68c278ebee5d) and results in a 40% speedup (on doc-gen4). This looks great to me! Feel free...

> The ergonomics are so bad that they even implemented a server more now for sbt, where you have an sbt server instance running in the background and `sbt foo`...

@gebner I'm sorry, but I am not sure what you mean. Lake does log the executed `lean` command and its stout and stderr. Are you not seeing that? Or is...

Okay, makes sense. I will put this on my todo list. Currently, no information is kept about the failing build task, so doing either of these will require some major...

@gebner > ``` > Found dependency `std` > `mathlib` locked `main` at `274cf5a5f906852b96bd8f4b045b243f2717edaf` > Using `main` at `23f8577169c049e6eb472a0354c11b9b934b4282` > ``` > > Note that the update for `std4` is not...

This is non-trivial to add, but it is a good suggestion and something I will put on my TODO list. Ironically, doing this for the example you mentioned (i.e., package...

@gebner Thanks for the PR, especially the updated test! 😄 However, this does not actually fix the underlying issue. First, removing the check does not result in Lake copying the...