Zulip Chat Archive

Stream: new members

Topic: Installation


Dan Velleman (Oct 25 2021 at 18:51):

I just attempted to install Lean 4, but I don't think it's installed properly. I started a file with "import data.real.basic" and got an error message "unknown package 'data' ". What am I doing wrong?

Mario Carneiro (Oct 25 2021 at 19:01):

That's lean 3

Mario Carneiro (Oct 25 2021 at 19:02):

an import that exists in lean 4 is import Std.Data.HashMap

Dan Velleman (Oct 25 2021 at 19:02):

Thanks.

Kevin Buzzard (Oct 25 2021 at 19:02):

If you want to do mathematics then start here with Lean 3.

Kevin Buzzard (Oct 25 2021 at 19:03):

Right now the big maths library is Lean 3 only; this will change, but not for a few months at least.

Dan Velleman (Oct 25 2021 at 19:04):

Is there a list of imports that exist in Lean 4?

Dan Velleman (Oct 25 2021 at 19:04):

Is it possible to have both Lean 3 and Lean 4 installed and switch between them?

Kevin Buzzard (Oct 25 2021 at 19:05):

Yes

Kevin Buzzard (Oct 25 2021 at 19:05):

Each Lean repository has a file in the root directory which says exactly which version of Lean it compiles against

Kevin Buzzard (Oct 25 2021 at 19:06):

For example here is the file corresponding to a repository I've done some work with -- the file says it uses Lean 3.34 and also a specific commit of mathlib, Lean 3's maths library. On the other hand I can also open another github repo which says it works with Lean 4 (e.g. this file in a Lean 4 repo) and this just works out of the box too.

Dan Velleman (Oct 25 2021 at 19:13):

I see there's something called mathlib4 at GitHub. Is that the Lean 4 library? Was it supposed to be installed on my computer as part of the Lean 4 installation? Or is there something I'm supposed to do to install it?

Kevin Buzzard (Oct 25 2021 at 19:13):

mathlib4 is a playground for experimenting with manual ports of part of mathlib, Lean 3's maths library,

Kevin Buzzard (Oct 25 2021 at 19:14):

If you installed Lean 4 then all you got was Lean 4. You can clone repos from github and work on them, although the actual procedure for how to do this is changing rapidly right now (e.g. I don't think I know how to do it myself right now with Lean 4).

Dan Velleman (Oct 25 2021 at 19:15):

I installed Lean 3 first and played with it a little bit, but I have a project that I think is going to need to be done in Lean 4, so I installed that. I don't know if I still have Lean 3, or how to go back to it if I do.

Kevin Buzzard (Oct 25 2021 at 19:16):

There is something called lakefile.lean in mathlib4 as of a week ago, and this is some kind of "Lean makefile" but I don't know any more than that (although there are oodles of details in the #lean4 stream about it)

Kevin Buzzard (Oct 25 2021 at 19:16):

What's the nature of your project?

Kevin Buzzard (Oct 25 2021 at 19:17):

Both Lean 3 and Lean 4 can certainly coexist on a machine and there won't be any problems; a little program called elan will do the job of deciding which version of Lean you will be using.

Kevin Buzzard (Oct 25 2021 at 19:18):

buzzard@bob:~$ cd active-lean-projects/
buzzard@bob:~/active-lean-projects$ cd mathlib4
buzzard@bob:~/active-lean-projects/mathlib4$ lean --version
Lean (version 4.0.0-nightly-2021-07-27, commit 0bea52d1b535, Release)
buzzard@bob:~/active-lean-projects/mathlib4$ cd ..
buzzard@bob:~/active-lean-projects$ cd mathlib
buzzard@bob:~/active-lean-projects/mathlib$ lean --version
Lean (version 3.33.0, commit a0fb1e8c7ac8, Release)
buzzard@bob:~/active-lean-projects/mathlib$

Works by magic

Dan Velleman (Oct 25 2021 at 19:21):

If I understand the commands you displayed, different projects can use different versions of lean. But then how do I determine which version of Lean a project will use?

Dan Velleman (Oct 25 2021 at 19:26):

Are there completely different procedures for creating projects in Lean 3 and Lean 4? It looks like in Lean 3 I'm supposed to use leanproject new, and in Lean 4 I'm supposed to use leanpkg init. Is that right?

Kevin Buzzard (Oct 25 2021 at 19:27):

If you're downloading the package from github then you look in the leanpkg.toml or (for projects which are only a week or two old) then lean-toolchain file (so it seems -- I don't know anything about this file). Yes, there are completely different procedures for creating projects in Lean 3 and Lean 4. leanproject is supposed to be a one size fits all so-easy-even-mathematicians-can-use-it program which sets up Lean 3 projects.

Kevin Buzzard (Oct 25 2021 at 19:27):

We'll worry about making Lean 4 project initialisation so easy even mathematicians can do it once we've solved the problem of porting the maths library. You didn't say what the nature of your project was.

Dan Velleman (Oct 25 2021 at 19:33):

Sorry, it is not "so-easy-even-mathematicians-can-use-it." I just tried the command "leanproject new <project name>", which I thought was what I was supposed to use to create a Lean 3 project, and got an error message: "uncaught exception: Lean package manager, version 4.0.0"

Kevin Buzzard (Oct 25 2021 at 19:37):

I suspect that's because you've run it inside a directory which contains some lean 4 files

Kevin Buzzard (Oct 25 2021 at 19:38):

Mathematicians aren't supposed to be messing with lean 4 yet :-)

Dan Velleman (Oct 25 2021 at 19:39):

OK, I'll try in a different directory. Thanks for all your help.

Kevin Buzzard (Oct 25 2021 at 19:39):

Just like a file explorer, the command line knows which directory it's in. You want to make sure that it's in C:/my_lean_projects or whatever

Kevin Buzzard (Oct 25 2021 at 19:41):

(ps just to be clear, I am unashamedly a mathematician)

Jeremy Avigad (Oct 25 2021 at 19:45):

Both Lean installation instructions install a program called elan which magically decides which version of Lean to run, and even fetches it if necessary. When you are in a directory that has been set up right with a leanpkg.toml file, it uses that information to determine the right version. If you type elan at the command line, you can see some options. For example, elan show will show you all the versions of Lean that it has fetched over time. You can say e.g. elan default leanprover-community/lean:3.32.1 to set a specific default, but it should be overridden by a toml file when there is one. Note that typing lean really runs elan. If you type lean --version, it will tell you which version of Lean is being run.

Eric Wieser (Oct 25 2021 at 20:19):

Perhaps leanproject should run lean --version and check it's on Lean 3, assuming it doesn't know anything about lean 4

Dan Velleman (Oct 25 2021 at 21:18):

Thanks Jeremy. When I type elan show I get the following list of installed toolchains:
stable
leanprover-community/lean:3.26.0
leanprover-community/lean:3.33.0
leanprover/lean4:stable (default)

You say that Lean will use the right version in a directory with a leanpkg.toml file. OK, so how do I set up a directory with such a file to use Lean 3? The Lean 3 instructions for setting up a project say to use the command leanproject new <name>, but that now gives me an error message. The Lean 4 instructions for setting up a project say to use the command leanpkg init <name>. That command doesn't give an error message, but the leanpkg.toml file it creates says nothing about what version of Lean it should use. I can see in the mathematics_in_lean leanpkg.toml file how the lean version should be specified. Do I have to open my .toml file and add a "lean_version" line?

Maybe I should just use elan default to go back to Lean 3 and stick to that for the moment.

I'm sorry if I sound a little frustrated, but when I try to follow the installation instructions, nothing works as described online.
I often get error messages, and the instructions give almost no information about what to do when you get error messages.

Kevin Buzzard (Oct 25 2021 at 21:23):

The instructions for lean 3 should be fine for lean 3 projects. Can you be more specific about the problem you're having with leanproject new my_cool_project? Saying "it gives me an error message" isn't very helpful

Dan Velleman (Oct 25 2021 at 21:25):

Here's the error message:
uncaught exception: Lean package manager, version 4.0.0

Usage: leanpkg <command>

init <name> create a Lean package in the current directory
configure download and build dependencies
build [<args>] configure and build *.olean files

See leanpkg help <command> for more information on a specific command.
Command '['leanpkg', 'new', 'HTPI']' returned non-zero exit status 1.

Kevin Buzzard (Oct 25 2021 at 21:25):

If the directory you're running this command in, or if any directory containing this directory as a subdirectory, contains a leanpkg.toml file, then there will be trouble of this nature

Eric Wieser (Oct 25 2021 at 21:26):

This looks like a bug in leanproject to me

Eric Wieser (Oct 25 2021 at 21:26):

If you have lean4 as a default and no existing projects, then when leanproject calls out to leanpkg init internally, it's in for a shock

Kevin Buzzard (Oct 25 2021 at 21:26):

Can you also confirm which version of leanproject you're using, with leanproject --version?

Kevin Buzzard (Oct 25 2021 at 21:27):

Maybe the issue is simply that when you installed lean 4 the default lean changed and you have to manually change it back using elan?

Dan Velleman (Oct 25 2021 at 21:28):

There's no leanpkg.toml file in either this directory or any directory that contains it (although there are leanpkg.toml files in another subdirectory of the directory containing this directory). I'll try changing my default and see if that solves it.

Kevin Buzzard (Oct 25 2021 at 21:29):

I'll get to a computer and see if I can reproduce. Toml files in other subdirectories should be fine, I have those too (all my lean 3 and lean 4 repos are in a lean-stuff directory)

Dan Velleman (Oct 25 2021 at 21:34):

OK, I changed my default to leanprover-community/lean:3.33.0, and now leanproject new <name> seems to work.

Kevin Buzzard (Oct 25 2021 at 21:34):

Indeed I can confirm that having elan default to a Lean 4 binary breaks leanproject. Hopefully you can fix it with elan default leanprover-community/lean:3.33.0 and then leanproject new my_cool_project should hopefully eotk.

Kevin Buzzard (Oct 25 2021 at 21:34):

@Patrick Massot I have a vague memory that this came up before...

Dan Velleman (Oct 25 2021 at 21:38):

Does every project contain a copy of mathlib? I wasn't expecting that.

Kevin Buzzard (Oct 25 2021 at 21:38):

Every project you make with leanproject does because it's supposed to be mathematician-proof

Kevin Buzzard (Oct 25 2021 at 21:38):

You can just remove it if you want -- do you want to know how?

Kevin Buzzard (Oct 25 2021 at 21:39):

It involves manually editing leanpkg.html and then deleting _target

Kevin Buzzard (Oct 25 2021 at 21:40):

You leave the [dependencies] line but delete the mathlib = ... line after it

Kevin Buzzard (Oct 25 2021 at 21:40):

I've asked several times what you're planning on doing, but because you never responded I can't give any advice on whether this would be a good or bad idea for you

Eric Wieser (Oct 25 2021 at 21:41):

To be clear; are you surprised that new projects depend on mathlib, or that that dependency is handled by making a full copy?

Kevin Buzzard (Oct 25 2021 at 21:41):

mathlib isn't just a maths library, it contains a lot of useful tactics too.

Eric Wieser (Oct 25 2021 at 21:42):

Also non-mathlib lean3 core gets smaller and smaller; currently Yaël is PRing removing integers from core!

Dan Velleman (Oct 25 2021 at 22:03):

Kevin: Perhaps I shouldn't have said "project". More of a vague, unformed idea at the moment, and I didn't want to try to explain. At this point, I'm just trying to learn Lean.
Eric: I'm not surprised that new projects depend on mathlib, but I assumed that there would be one copy of mathlib on my computer in a place that is accessible to all projects. Perhaps the issue is that mathlib changes often, so there isn't a single, stable "mathlib" that all projects can use?

Kevin Buzzard (Oct 25 2021 at 22:04):

Yes that's exactly it -- mathlib master can change 10 times a day and as it grows people want to use the latest features. I probably have 50 copies of mathlib on the machine I'm typing on now

Kevin Buzzard (Oct 25 2021 at 22:04):

and they're probably all different

Dan Velleman (Oct 25 2021 at 22:04):

Got it. Thanks.

Kevin Buzzard (Oct 25 2021 at 22:06):

Here is what I'm subjecting the 1st year UGs at my university to, and here is what I subjected some PhD students to earlier this year (all mathematicians)

Kevin Buzzard (Oct 25 2021 at 22:06):

And if you want something more type-theoretic then #tpil is a fantastic resource

Dan Velleman (Oct 25 2021 at 22:08):

Thanks Kevin.

Kevin Buzzard (Oct 25 2021 at 22:09):

My stuff is often quite alegbraic -- the official tutorials are more analytic

Yaël Dillies (Oct 25 2021 at 22:48):

Eric Wieser said:

Also non-mathlib lean3 core gets smaller and smaller; currently Yaël is PRing removing integers from core!

Not to lower your expectations, but I think this is not happening :sad:
I got terribly misled by faulty docgen.

Yaël Dillies (Oct 25 2021 at 22:49):

In particular, they are used for widgets, which I think should stay in core?

Patrick Massot (Oct 26 2021 at 07:21):

It's true that leanproject was written long before Lean4 came out and it was never updated to cooperate with Lean 4. PRs are welcome. Also note that you can actually have a central copy of mathlib used by all projects, this is explained in the documentation. But it's so useless (for reasons explained by Kevin) that nobody does it.


Last updated: Dec 20 2023 at 11:08 UTC