RFC: specify `--packages` to lake using an environment variable

Proposal

lake currently supports specifying a package overrides JSON file only via the --packages argument, which makes it clumsy to use lake in a wrapped way, e.g. when working in a local development environment with packages installed via Nix (as leanPackages was added recently to nixpkgs).

My proposal is to add a LAKE_PACKAGES environment variable to specify package overrides with lower precedence than --packages.

Another RFC suggests adding a separate system for handling packages installed via the system package manager. As noted in this comment in the RFC this option is not needed for building on Nix as lake already has the package overrides feature. A later PR to nixpkgs uses the --packages option to build lake packages.

I believe (and have verified to some extent, more on this later) that the user experience of setting up a development environment with LAKE_PACKAGES pointing to dependencies that have already been built is significantly better than constantly passing --packages to lake. These are the primary improvements:

• No need to make changes to the VS Code lean extension to work with a wrapped lake --packages as the extension fails with strange errors.
• The option propagates to subprocesses that may use lake directly. The wrapper argument doesn't get propagated because of the way the lean server spawns lake. If my understanding is correct, it looks for the unwrapped lake binary and sets LAKE according to that rather than using the wrapper.
• Running lake build in the development environment just works. No need to pass --packages or create a wrapper for that.

What I mean by "development environment" is roughly a customized set of PATH and other environment variables. On Nix, one typically uses nix-shell to enter a development environment.

Even without this proposal, we have already achieved getting lake to not download or build any of the dependencies (after they have been cached by Nix).

Even though it sounds like it, this request is not nix-centric; other package managers and development environment setups will probably also benefit from this.
Maintainability should not be a problem as this doesn't essentially add new code branches.

Demo

I'm working on a repository to demonstrate how this feature interacts with a Nix development shell and will update it here once it's ready.

Community Feedback

There hasn't been any discussion on this yet.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start by tracing how lake currently reads the --packages argument and how that value is passed to subprocesses. Add LAKE_PACKAGES with lower precedence than --packages, then verify that ordinary lake commands and subprocesses use the environment-provided package overrides without requiring the argument.