Gabriel Ebner

> That is, what would you like Lake to do with this information? I think the ultimate goal is clear: `Base.olean` should be recompiled if `style.css` changes. The rest is...

> Ah, are you saying that if `Base,lean` _does not change_ but `style.css` does, Lake should then perform a rebuild of `Base.lean` (using the information about dependencies it obtain from...

> > 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? It's not really a...

> > 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...

One more: *Call lake less often.* This doesn't really help with command-line usage, and I don't think we should implement an sbt-style repl for lake. But we could conceivably eliminate...

> > _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 to PR...

> Lake does log the executed lean command and its stout and stderr. Are you not seeing that? Yes, it does indeed log the executed lean command. But only above...

> it's still an issue in the latest release Only partially. See #120 It turns out this already worked in some cases. Namely `lake update` would pick up changes in...

Another issue: when updating `mathport` this happened: ``` git clone https://github.com/leanprover-community/mathport cd mathport git checkout db81206678e7a632e6a6490c680f4c466436b09d lake update ``` Output: ``` Found dependency `Cli` `mathlib` locked `master` at `112b35fc348a4a18d2111ac2c6586163330b4941` Using...

Oh that is indeed an issue. I think I got confused by the two meanings of `shouldUpdate` here (are we inside `lake update` vs. should we do a `git pull`)....