Installation

Stream: new members

[Dan Velleman]

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]

That's lean 3

[Mario Carneiro]

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

[Dan Velleman]

Thanks.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Dan Velleman]

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

[Dan Velleman]

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

[Kevin Buzzard]

Yes

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

What's the nature of your project?

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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

[Dan Velleman]

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

[Kevin Buzzard]

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]

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

[Jeremy Avigad]

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]

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

[Dan Velleman]

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]

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]

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]

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]

This looks like a bug in leanproject to me

[Eric Wieser]

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]

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

[Kevin Buzzard]

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]

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]

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]

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

[Kevin Buzzard]

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]

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

[Dan Velleman]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

It involves manually editing leanpkg.html and then deleting _target

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Eric Wieser]

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

[Dan Velleman]

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]

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]

and they're probably all different

[Dan Velleman]

Got it. Thanks.

[Kevin Buzzard]

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]

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

[Dan Velleman]

Thanks Kevin.

[Kevin Buzzard]

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

[Yaël Dillies]

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]

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

[Patrick Massot]

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.