RFC: lake build: add `--system-packages` flag to use system package manager

Proposal

In order for lean libraries to be packaged for Linux distributions, they must be installable using the system package manager. The system package manager will use lake build for building individual projects, but will manage the dependencies without lake. There should be a way for lake build to either:

build the project without considering dependencies (and assume they will be made available at runtime using $LEAN_PATH or some other method)
specify one or more package directories on the command-line for lake to use at build-time

Notes:

The exact implementation (flag vs. environment variable, how to specify multiple paths, etc.) is not important, system package managers are flexible there.
Patching lakefile.lean/toml manually for each library is not feasible.
Fetching any information at build time from a remote endpoint (like the reservoir registry) or via git fetch is also not OK for reproducible package managers like Nix or Guix.
Ideally lake would be able to link directly against compiled .olean/.lean files, and not require the original code or lakefile.lean for dependencies. Not a big deal if this isn't possible.

Community Feedback

The system package manager problem was mentioned here, although the issue itself was for a different idea: https://github.com/leanprover/lean4/issues/3193#issuecomment-1898009228

Impact

The impact would be availability of Lean libraries on various Linux distributions.

I have Lean 4.10, batteries, and some other libraries packaged for Guix via a new lean-build-system. But I cannot package mathlib because lake keeps trying to git fetch the dependencies.

leanprover / lean4