feature request: `lake install`

[kim-em]

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.

[nomeata]

You can add loogle to that list.

[austinletson]

lake install lean4checker will be useful for ci as in #3950

[tydeu]

Related discussion on Zulip: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Omit.20compilation.20and.20run.20the.20executable.20binary.20in.20the.20.2Elake/near/468564582