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

[a2379]

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:

1. build the project without considering dependencies (and assume they will be made available at runtime using $LEAN_PATH or some other method)
2. 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:
#3193 (comment)

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.

[Coda-Coda]

This sounds like a good idea to me! 😃

[divyaranjan1905]

Hello @Coda-Coda @a2379 , has this been fixed?

[hargoniX]

No, it is also currently not recommended to package Lean with a system package manager as libraries currently rely on very specific releases and are often not forward or backward compatible. For example if you install Lean version 4.x and then work on a mathlib checkout that relies on 4.y you are just going to get lots of weird errors.

[divyaranjan1905]

No, it is also currently not recommended to package Lean with a system package manager as libraries currently rely on very specific releases and are often not forward or backward compatible. For example if you install Lean version 4.x and then work on a mathlib checkout that relies on 4.y you are just going to get lots of weird errors.

I see, that makes sense, but in a transactional package management/distribution setting like Guix or Nix, the curl method doesn't work because it demands write access to read-only directories such as ~/.profile.

[a2379]

No, it is also currently not recommended to package Lean with a system package manager as libraries currently rely on very specific releases and are often not forward or backward compatible. For example if you install Lean version 4.x and then work on a mathlib checkout that relies on 4.y you are just going to get lots of weird errors.

Sure, but that is not what the original issue is referencing. Lake should support installing both Lean and Lean libraries through the system package manager. Version mismatches would not be an issue, because package maintainers are used to updating programs and their dependencies in lockstep.

[divyaranjan1905]

@hargoniX and other maintainers, at least you might guide us on how this might be implemented in a PR? Because without this, mathlib et.al simply would be unusable in distros such as Guix.

[nomeata]

I believe there is on the roadmap the ability to vendor the dependencies, and then build without network access. This would presumably already help a bunch for your use case? (Can't comment on timelines or precise form of the feature.)

[divyaranjan1905]

I believe there is on the roadmap the ability to vendor the dependencies, and then build without network access.

Indeed, that would be all we need.