lean4 installs files into a non-standard location src/lean

[yurivict]

Prerequisites

• [X] Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

Files can't be installed under src/. They should be pushed into share/lean4 to be compatible with directory structure conventions.

Context

I am trying to create the FreeBSD port for lean4, and the src directory is not allowed.

Versions

4.5.0-rc1

[nomeata]

Hello, and thanks for helping to make lean4 available to FreeBSD users!

There is a related issue at https://github.com/leanprover/lean4/issues/3068.

TL;DR: lean4 is (currently) unsuitable for distribution packaging. It moves too quickly, and developers expect to use precisely the version of the lean4 compiler that is pinned (via lean-toolchain) by the project they are working on.

This will change in the future, but at the moment packaging and distributing lean4 will probably be a disservice to the users.

What is very useful is to package elan, the tool that users use to manage the lean4 toolchain.

Because we currently don’t support packaging and distribution outside of elan, we won’t (for now) work on “installing lean”. Of course, your port could patch and move files as you see fit.

BTW, does lean even run well on FreeBSD? I wonder if the mmap semantics used when mapping oleans are portable neough.

[yurivict]

What is very useful is to package elan [...]

elan probably assumes that pre-built binaries are ailable for the platform, which would probably be impractical for FreeBSD.

BTW, does lean even run well on FreeBSD?

It runs, except for 6 failing leanlaketest tests. I will look into them.

I wonder where are the files from src/ used, because I moved them to share/lean4/src and lean4 still runs fine.

[nomeata]

What is very useful is to package elan [...]

elan probably assumes that pre-built binaries are ailable for the platform, which would probably be impractical for FreeBSD.

Oh, right, didn't think that part through :-D

BTW, does lean even run well on FreeBSD?

It runs, except for 6 failing leanlaketest tests. I will look into them.

I wonder where are the files from src/ used, because I moved them to share/lean4/src and lean4 still runs fine.

I don't actually know.

[digama0]

Which src/ are we talking about here? Can you give an examples of some files you see?

[yurivict]

It installs files like src/lean/lake/Lake/Config/Opaque.lean, src/lean/lake/tests/lock/Nop.lean and src/lean/lake/tests/badImport/X.lean.

I am not sure if this is intentional.

[digama0]

Those are actually source files though? They are there because lean needs to be able to find them for go-to-definition to work properly. (The test files are probably not necessary but it's presumably easier to just copy the whole directory than select only the lean files and maybe the README and LICENSE files.)

What is the absolute path of these files? I don't understand if you are asking for the lean4 repo itself to move files around or whether this is about files being unpacked by elan inside the .elan directory or something else... Having project sources in the src/ directory is a very normal thing so I don't really understand the request.

[yurivict]

Having project sources in the src/ directory is a very normal thing so I don't really understand the request.

cmake installs them into /usr/local/src which isn't allowed by conventions. They should be moved under share/lean4.

If these files are used, it isn't clear why didn't any tests fail. Is the functionality using these files not tested?

[digama0]

How are you invoking lean / cmake such that things are written into /usr/local/src? As mentioned above, the standard layout is to have lean installs in the HOME/.elan folder because people have to be able to switch between multiple lean versions.

[yurivict]

I just configure with cmake and then run gmake && gmake install.

[kim-em]

That's not really a supported method of using Lean. We advise all users to use elan for obtaining binaries. So if you want to make Lean easier to use on a currently unsupported system, you can help with packaging elan for distribution, or think about how we could easily provide binaries for more systems. But realistically, if we can't build the binaries that elan looks for within our Github CI process, it may be better to think about how users could compile locally and put the binaries in HOME/.elan. Anything that is installing Lean elsewhere is only going to provide a broken experience for users.

[yurivict]

@semorrison Are there binaries available for FreeBSD?

[kim-em]

No, they are not. You can see the binaries we produce by looking at a release page, e.g. https://github.com/leanprover/lean4/releases/tag/v4.5.0-rc1.

doc/setup.md describes the supported platforms. You can see there that there is a currently commented out section for "Tier 3" platforms, which hopefully could have FreeBSD added.

It's important to understand @digama0's comment above, that installing a fixed version of Lean is currently not helpful to users. It's essential that any packaging efforts result in the user having a usable copy of elan, even if on unsupported platforms there are extra steps to provide elan with binaries.

[yurivict]

Also binaries are significantly less secure than building from source. They can contain malware. They can be substituted in the download process. Many people are binary-averse.

[yurivict]

Your idea of limiting people to binary downloads will definitely meet a lot of resistance, and rightfully so.

[kim-em]

Sorry, I didn't at all intend to say that you can only use binaries we provide! Of course anyone can build from source, and that will always be the case.

The key sentence in my initial message about is:

it may be better to think about how users could compile locally and put the binaries in HOME/.elan

I'm just trying to explain that if you build from source, putting the compiled lean binary in some global local is not a useful thing for 99% of users. Instead that compiled (whether compiled locally from source or via our CI) binary needs to go somewhere that elan can find it (usually ~/.elan), so that elan can dispatch to the appropriate toolchain depending on what version of Lean a particular project requests. Does that make sense?

The fact that the CMakeLists.txt file has a code path for putting the Lean binary in a global location is, as far as I understand, an old artifact that is not useful for most of Lean's users (including those users on unsupported platforms).

[yurivict]

[...] elan can dispatch to the appropriate toolchain depending on what version of Lean a particular project requests.

What might be the choices for the version of Lean in a particular project? Do they correspond to tags, like 4.3.0 vs. 4.4.0, or do they differ by Lean build options? In other words, why should there be multiple versions of Lean available at the same time?

[digama0]

They correspond to tags like 4.3.0 or 4.4.0. (Lean releases can be found at https://github.com/leanprover/lean4/releases, but there are also PR releases for testing and nightlies.) Lean is a rapidly changing beast, and the way the community handles this is by pinning the version of the compiler used to compile a given project in a lean-toolchain file, e.g. https://github.com/leanprover/std4/blob/main/lean-toolchain . It is essential that this mechanism works for a smooth user experience, because projects are not always all on the same version of lean (and neither are branches within the project) and most users have a handful of leans installed simultaneously. Currently lean releases a new release candidate about once per 1-2 weeks, and mathlib updates every time, meaning that many PRs will see one or more version bumps while the PR is still being reviewed. elan manages these installs and ensures that the right one is used on a given project.

Build options are essentially never used by users, unless they are pre-set in the CI which cuts a release. For example, the USE_GMP cmake option is only set on architectures which have GMP available. Industrial users may also have a custom build of lean to disable this flag due to license restrictions.

[yurivict]

Thank you for this information. This makes sense.

So when users would like to use the latest version of Lean4 on FreeBSD - they would be able to use the package lean4 built from the port math/lean4. And when users would need to use older versions - they would use elan that is now also available. This would work assuming binaries would be available somewhere, which isn't currently the case.

[digama0]

I think a feature that would help a lot for your use case is if elan could learn how to build from source instead of using binaries, either because no binary release is available or because the user is binary-distribution-averse. (Users may also be internet-distribution-averse, but I think solving this is significantly harder.) For the present the workaround would be to check out the right version of lean4, build it, and then copy the distribution into the elan folder. Users would have to repeat the process whenever they want a new version.

[juhp]

It may well make sense to install lean4 under say $libdir/lean4/ for now. Then add symlinks to the system bindir say. I am considering trying that for Fedora anyway (ie use /usr/lib64/lean4/ as an install prefix).