lean4
lean4 copied to clipboard
leanprover
Package manager that works smoothly on Linux/OSX/Windows
The goal is to have something like Rust Cargo. https://github.com/rust-lang/cargo It should be implemented in Lean. Core developers will help with missing APIs.
Fyi, I posted a thread on Zulip (leanpkg++ idea) related to a design idea for the new leanpkg. The basic idea is for developers to write package configuration in Lean itself rather than through something like leanpkg.toml. This would make builds in Lean much more flexible and allow for leveraging Lean's extensive metaprogramming capabilities in package managment. The idea seems to have some support, so it might be worth looking into.
The idea seems to be related to FAKE from F# or the Zig language as per the mentioned thread.
Hey all, I am just starting to learn Lean and wanted to give my perspective coming from the Python community, that sticking with a declarative package instead of using Lean to specify dependencies might have advantages.
The Python folks have spent a long time moving away from package information as code (setup.py) to declarative files (pyproject.toml) (emphasis mine):
The traditional setuptools way of packaging Python modules uses a setup() function within the setup.py script. Commands such as python setup.py bdist or python setup.py bdist_wheel generate a distribution bundle and python setup.py install installs the distribution. This interface makes it difficult to choose other packaging tools without an overhaul. Because setup.py scripts allowed for arbitrary execution, it proved difficult to provide a reliable user experience across environments and history.
PEP 517 therefore came to rescue and specified a new standard to package and distribute Python modules. Under PEP 517:
a pyproject.toml file is used to specify what program to use for generating distribution. [...]
With this standard, switching between packaging tools becomes a lot easier. build_meta implements setuptools’ build system support.
@saulshanabrook I agree that declarative specification of dependencies is useful. However, I think that can be accomplished even with an interpreted configuration through the use of a lock file. Also, it should be noted that even in the case you described, the build system is still written in Python -- it is only dependency listing itself that is declarative (making it much the same as a lock file).
One other thing to note is that unlike python, where there is a pretty straightforward mapping between a package and an import, a package in Lean may end up containing many other things besides the module itself, and those things may wish to be configurable via scripting. For example, Lean package may even end up containing scriptable, custom UI widgets that may also wish to be configurable via the package script.
TL;DR Dependencies should ideally have a declarative listing. Other package management tasks (i.e., builds and complex configurations) need interpreted scripting.
The idea seems to be related to FAKE from F# or the Zig language as per the mentioned thread.
zig v0.11.0 releases zig-pkg initial support [WiP].
- https://github.com/ziglang/zig/pull/14265
