Installing lean from a linux distro

Stream: new members

[Eric Wieser]

Zack Weinberg said:

Any/all advice would be appreciated, except please don't tell me I should use mathlib, because I can't use mathlib, because of ProofWidgets4#115.

I think you should use mathlib :). By which I mean, I think you should ask for help with the issue you linked, because it sounds like an issue with your installation not with proofwidgets

[Kevin Buzzard]

You should not be using your distro's version of Lean. This causes no end of problems. You might not like this but that's a fact. Lean's ecosystem is not suitable for installation via a distro. Lean updates several times a month; mathlib updates several times a day. Distros simply cannot keep up. elan, Lean's package manager, solves this problem. Your distro's package manager does not. Different Lean packages use different versions of Lean and of mathlib and your local ecosystem needs something which can install an arbitrary lean/mathlib combination at any point. elan is that thing. A fixed binary coming from a distro is the exact opposite of this, so you cannot get anyone else's code working (e.g. proofwidgets in your case). Note everyone else's response to your issue -- "it's working fine for me".

[Kevin Buzzard]

@jthulhu you were recently asking for examples of problems caused by distributing Lean via a distro's package manager. See https://github.com/leanprover-community/ProofWidgets4/issues/115 and the above thread (someone failing to do something basic because they have given up getting the maths library working and are now in even worse trouble trying to work around this) because they installed Lean via a distro. You are contributing to this mess.

[Kevin Buzzard]

@Zack Weinberg I would be interested to know which distro is shipping a Lean package which has caused you all these problems. I would also recommend that you pointed whoever uploaded that package oto your distro, to this thread.

[Kevin Buzzard]

One day the ecosystem will settle down, but that day is not today.

[Ryan Lahfa]

Kevin Buzzard said:

jthulhu you were recently asking for examples of problems caused by distributing Lean via a distro's package manager. See https://github.com/leanprover-community/ProofWidgets4/issues/115 and the above thread (someone failing to do something basic because they have given up getting the maths library working and are now in even worse trouble trying to work around this) because they installed Lean via a distro. You are contributing to this mess.

I get the frustration, but distro packaging isn’t the problem — it’s a normal and reasonable way people install software on Linux. Blaming users for using their system package manager doesn’t help. If Lean builds from distros break mathlib or Lake, maybe we should detect that at build or runtime (e.g., via a LEAN_FROM_DISTRO flag) and give users a clearer message. People won’t stop asking for distro packages — and they shouldn’t. Let’s focus on making the failure mode better instead of shaming users for trusting their systems.

Kevin Buzzard said:

Zack Weinberg I would be interested to know which distro is shipping a Lean package which has caused you all these problems. I would also recommend that you pointed whoever uploaded that package oto your distro, to this thread.

Well, from what I usually see from Zack, it's most likely NixOS where we ship multiple versions of Lean in-tree. There's usecases for NixOS users where elan doesn't work and will not work.

[Mario Carneiro]

Ryan Lahfa said:

If Lean builds from distros break mathlib or Lake, maybe we should detect that at build or runtime (e.g., via a LEAN_FROM_DISTRO flag) and give users a clearer message. People won’t stop asking for distro packages — and they shouldn’t. Let’s focus on making the failure mode better instead of shaming users for trusting their systems.

I don't blame the users, I blame the distros and package maintainers that ignore the community here and package lean despite explicit instructions not to do so for the distro, resulting in problems that we have to clean up later

[Kevin Buzzard]

Having heard from the packagers in other threads, I'm now wondering if there is a middle ground which is not "tell the distros to not do this" and is closer to "tell the distros to do it properly".

[Julian Berman]

The "do it properly" is essentially to offer packaging elan, and some do (e.g. homebrew), but the middle disappears once the discussion turns to packaging a fixed Lean version. Personally I understand Lean's viewpoint but as a user I very much appreciate distros fighting the good fight here a bit. Ultimately as a user, I do personally want my installs going via my package manager, not a language specific package manager. And I do not see distros in general listening to us (now the Lean community) saying "don't package this" -- this was the experience with Homebrew as well where they were happy to package elan but not happy to not package lean. And yes this creates burden on languages (and their communities) which want to manage the installation and user experience themselves, Lean not being the first to have these kinds of issues, and yes it creates extra work and frustration on all sides when new users run into issues. I blame no one in the equation, but I don't think it's realistic that distros will stop packaging fixed versions, part of their job is to be a trust root for users who do not want to trust each communities' build processes or peculiarities. In the long run I think as the language stabilizes everyone gets less frustrated.

[Eric Wieser]

Maybe the first step here is that info: no Elan detected; you will need to manually restart Lake should just be an error if lean --version doesn't match the toolchain version

[Zack Weinberg]

In this case I'm actually using Gentoo, and it looks to me like nobody has been bothered to update their packaging of Lean in Quite Some Time. They have lean 4.11 and 4.14 and nothing newer, and no packages of either mathlib or elan. I switched to installing via elan and, indeed, i can install mathlib into a project now.

However, I feel that I should not have had to do that. Actually I'd like to make a much stronger statement: Ultimately, what I'm trying to do with Lean is to prove the equivalence of two functions (taken from a more conventional programming language, but both are proper mathematical functions). The pencil-and-paper proof requires nothing more than grade-school algebra on inequalities. IMNSHO, for a short proof that you could assign as homework in grade school algebra I shouldn't need mathlib, I shouldn't need an "up to date" version of Lean, and, last but not least, I shouldn't need anything like a "project".

In my ideal world I would ship my_function_equivalence.lean next to my_function_both_versions.c, without any further ceremony than that, and whoever receives a copy should be able to run lean my_function_equivalence.lean, again no more ceremony than that, using whatever version of Lean 4 they happen to have, to confirm that the proof within was valid.

[Eric Wieser]

Zack Weinberg said:

using whatever version of Lean 4 they happen to have,

Lean doesn't have nearly strong enough backwards compatibility guarantees for this to work, nor is having them a priority at this point in its life.

[Notification Bot]

12 messages were moved here from #new members > Beginner question: proofs involving Nat->Int conversions by Eric Wieser.

[Eric Wieser]

Zack Weinberg said:

IMNSHO, for a short proof that you could assign as homework in grade school algebra I shouldn't need mathlib

I think the rational numbers are part of most grade school algebra, but docs#Rat is not part of Lean itself