feat: `lake install`

[tydeu]

Creates a new CLI command lake install which adds a package to Lake's new toolchain-local package set. These packages are stored in a lake-packages directory in the current Elan toolchain and are available to all packages configured with Lake on that toolchain. This allows users to "install" Lean tools such as executables and facets which will then usable in every package without specifying said tool as a dependency. For example, doc-gen4 or import-graph would be useful tools to install.

Technical Note: Installed packages are loaded into the workspace after the current package's dependency tree. This means that if the same package is both installed and a dependency, the dependency version will appear in the workspace. Inversely, this means that Lake will first look into installed packages for executables / libraries before looking at the current package. For example, if two separate packages, one installed and one local, have a graph executable, Lake will run the installed one on lake exe graph.

Closes #3423. This change does not include the feature to automatically install the package on a toolchain switch because Lake does not currently have the version information to do this well. Namely, it needs a toolchain to compatible package version mapping to figure out what version to install.