trouble installing lean4 from source on Linux

[juhp]

Description

I am trying to package lean4 for Fedora: it builds but installation is not happening.

Steps to Reproduce

1. see https://github.com/juhp/lean4/blob/main/lean4.spec

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 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[nomeata]

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.

[juhp]

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/

[nomeata]

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?

[juhp]

I have haven't attempted packaging elan yet...

[semorrison]

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!)