Display how many files need to be rebuilt

Stream: general

[Yaël Dillies]

Now that oleans are rebuilt only when the user explicitly asks for it (Ctrl + Shift + X), I often find myself with a bit of a conundrum:

If the extension tells me there are missing oleans for dependency files, do I need to get cache or can I just quickly rebuild everything on my machine?

[Yaël Dillies]

The first situation usually happens after I switch branches and before I get cache. The second situation usually happens when I modify a file and then go to a later file. However there is a third case which can lead to either situation depending on the precise timing: If I switch branches, run lake exe cache get and quickly open the files I want to touch, they will tell me their dependencies are missing oleans. This could either mean that

• lake exe cache get hasn't finished running yet
• the file isn't covered by the cache (because the build stopped at an earlier file due to an error

[Yaël Dillies]

I believe the best way to distinguish between those two situations would be to display how many dependency files have out of date oleans. Note that that number would need to be recalculated every few seconds at least since we want to catch the point where lake exe cache get finishes unpacking the cache.

[Yaël Dillies]

What do people think?

[Kim Morrison]

Ideally lake build and lake exe cache get would just run cooperatively. One is CPU bound, one is network bound, so they needn't interfere at all. As oleans arrive over the network, cancel the local build file by file. Obviously this would require deep integration with lake, so isn't happening immediately. I do hope it will happen, though!

[Mario Carneiro]

it's even more complicated than that. In order to really take advantage of the parallelism I think it would be best to link to curl instead of just calling it in a fire-and-forget manner, so that you have full control over the communication pipeline and can launch new requests while old ones are still coming in. This is what I did in the lean-cache rewrite

[Michael Rothgang]

What's the state of that rewrite? I vaguely remember it being 5x faster, but blocked on design issues with lake - is that correct/still up to date?