Open juhp opened 9 months ago
Hallo Jens!
I guess “installing from source” isn’t a usecase we considered so far – users get lean from elan
, and we haven’t seen much distribution packaging yet.
In the CI scripts I find something like
cmake .. ${{ matrix.CMAKE_OPTIONS }} -DLEAN_INSTALL_PREFIX=$PWD/..
make -j4
make install
so running make install
in the right directory seems to be the right direction, it seems afterwards the directory
dir=$(echo lean-*-*)
contains the installation.
That said, it is not clear how useful it is to package lean4 itself for distributions yet. It is very fast moving, and most people want to use whatever revision of lean is pinned by the particular project they are working on.
It will be more useful as soon as programs built with lean want to enter distributions, of course.
What is useful is to package elan
(like rustup
): That is the usual entry-point to lean development.
Thanks, Joachim that helps indeed.
Though I still feel it would be good to fix cmake --install
to work as expected.
I am know I am "fighting the tide" but some people still prefer to use distro builds rather than upstream binary blobs.
I built packages for Fedora Linux (38, 39, Rawhide) and also EPEL 9 (RHEL) for x86_64, aarch64 and ppc64le: https://copr.fedorainfracloud.org/coprs/petersen/lean4/
I sympathize, I've been on that side as well, as you know :-). As soon as the time is right I will support the distro packagers needs.
Is elan already packaged?
I have haven't attempted packaging elan yet...
It seems packaging elan
everywhere would be the most useful thing at the moment. It means that people who want to use their distro packager have a way to use Lean, even if it not a full distro build, but it also means that they will be working in a compatible way with the ecosystem (in which every Lean project should be assumed to use a different toolchain!)
Description
I am trying to package lean4 for Fedora: it builds but installation is not happening.
Steps to Reproduce
Expected behavior: cmake --install to work
Actual behavior: cmake --install doesn't do anything
Additional information
Running
make install
in stage1/ seems to do something.Versions
Lean (version 4.3.0, Release) [OS version] Fedora Linux 39
Impact
Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.