Many Lean projects are development tools, and should not need to be upstream dependencies in order to use them in a project. Instead we need a lake install command, that registers a program as installed, and then provides a cache of binaries for that program, automatically building on requested toolchains as needed.

There are many projects that would make good use of this. shake, graph, and LeanCopilot being the more obvious ones.