Installing mathlib

Stream: new members

[Jasmin Blanchette]

Johannes H. helped me install mathlib on one of my machines, but now I can't remember what he did and I need to do it on two more machines.

The instructions at

https://github.com/leanprover-community/mathlib/blob/master/docs/elan.md

give two options, but neither "start a new package" nor "work on existing package" seems to convey what I want to do, which is simply to install mathlib so that I can use it from now on in any .lean files of mine (even if they don't themselves live in any packages). Any help or pointers would be appreciated.

[Johan Commelin]

Turn your home directory into a Lean package? [/joke]

[Patrick Massot]

There isn't much point in having Lean files that are not part of a project

[Patrick Massot]

But you can do it if you insist

[Jasmin Blanchette]

I can create a project.

[Jasmin Blanchette]

It's just that I didn't remember that Johannes did it for the other machine -- but maybe he did.

[Patrick Massot]

Assuming you installed elan, the next step is to install mathlib helper script:

curl https://raw.githubusercontent.com/leanprover-community/mathlib/master/scripts/remote-install-update-mathlib.sh -sSf | sh

Then, in order to create a new project depending on mathlib:

leanpkg new test
cd test
leanpkg add https://github.com/leanprover-community/mathlib
update-mathlib

[Patrick Massot]

this will create a new directory test containing a compiled copy of mathlib ready for use

[Patrick Massot]

inside test is src where you'll put your Lean code

[Patrick Massot]

I really need to update documentation. My teaching will be mostly over in three weeks, then I'll write a couple of late referee reports and then documentation will be wonderful...

[Johan Commelin]

Does leanpkg default to lean version 3.4.2 nowadays?

[Johan Commelin]

If not, you need to edit leanpkg.toml in test/ and fix the version. Otherwise update-mathlib doesn't work, which means you have to compile mathlib yourself.

[Patrick Massot]

Johan, please don't make things sound complicated

[Patrick Massot]

If Jasmin installed elan with default answer to all questions then he'll be fine

[Jasmin Blanchette]

I've used elan with default answers.

[Johan Commelin]

Last week things weren't fine when I helped Fabian

[Jasmin Blanchette]

I just checked on my laptop which Johannes installed and mathlib was installed as a component inside ~/.lean.

[Jasmin Blanchette]

I'll try to mimic that on the other machines.

[Patrick Massot]

That .lean is indeed used for lean files outside projects

[Jasmin Blanchette]

Thanks for your help and suggestions! If I can't sort it out, I'll come back or bug Rob.

[Patrick Massot]

But I don't think that update-mathlib, the script that fetches compiled mathlib, cares about such rogue Lean files, so it probably won't help you

[Jasmin Blanchette]

Hm... now I'm confused

[Jasmin Blanchette]

I think I'll ask Johannes.

[Patrick Massot]

Jasmin, it would really help us if you could try to the fives lines howto I wrote above.

[Patrick Massot]

If those five lines (6 if you include the line installing elan) are not enough then we need to know it

[Jasmin Blanchette]

OK let me try.

[Jasmin Blanchette]

You mean 1+ 4 lines, right?

[Patrick Massot]

yes

[Jasmin Blanchette]

It says: -bash: update-mathlib: command not found

[Jasmin Blanchette]

but what I don't like about it is that it requires creating a package

[Jasmin Blanchette]

with Johannes's approach it didn't

[Jasmin Blanchette]

which means I could freely use mathlib anywhere no questions asked

[Jasmin Blanchette]

and I'd like my laptops to be as similar as possible to each other

[Jasmin Blanchette]

so I'll try to reproduce what Jo did, I think -- it seems to correspond to neither of the two options listed online.

[Patrick Massot]

Did you source .profile after installing update-mathlib?

[Patrick Massot]

You can also indicate the full path $HOME/.mathlib/bin/update-mathlib

[Jasmin Blanchette]

I only blindly followed the instructions above. But OK sure I can try that.

[Patrick Massot]

I think the first line I wrote should have told you to do update your path by sourcing .profile

[Patrick Massot]

You should have seen the effect of https://github.com/leanprover-community/mathlib/blob/master/scripts/remote-install-update-mathlib.sh#L14-L16

[Jasmin Blanchette]

Sorry. Now I simply copied the entire .lean from one laptop to another and things work.

[Jasmin Blanchette]

It seems like .lean gets read automatically or something.

[Patrick Massot]

only if you are outside of all projects

[Jasmin Blanchette]

I don't want us to use projects in the course

[Jasmin Blanchette]

(I'm doing all of this for the Logical Verification course, which we started teaching in Lean last year.)

[Patrick Massot]

Won't you distribute Lean files to complete in this course?

[Jasmin Blanchette]

Yes, it will probably make sense to bundle them in a package

[Jasmin Blanchette]

but that's in November

[Jasmin Blanchette]

and students will have to create homework etc.

[Jasmin Blanchette]

I presume they'll be happier if they can install mathlib only once in .lean than in each package or something

[Jasmin Blanchette]

regardless, some people who are more Lean savvy will help me in due time with that (Alex B., Rob L.) -- pity Johannes H. is gone

[Jasmin Blanchette]

now, next problem: how come Isabelle doesn't build on two of my machines... ;)

[Johannes Hölzl]

didn't we use leanpkg install ...?

[Jan-David Salchow]

I just got my hands on a lean free mac, so I though I'd try if the install script works

[Jan-David Salchow]

The first step doesn't

[Jan-David Salchow]

there is brew on the computer, but no python

[Jan-David Salchow]

So read should ask me if I want to install python3

[Kevin Buzzard]

I tried installing Lean on a mac last week and the update-mathlib line didn't do anything either. In the end I just found the script and copy-pasted it.

[Jan-David Salchow]

Instead I get ```Jan-David.Salchow@C02Y13THJGH6:~:$ curl https://raw.githubusercontent.com/leanprover-community/mathlib/master/scripts/remote-install-update-mathlib.sh -sSf | sh
Installing python dependencies (at user level)
/usr/local/bin/brew

Jan-David.Salchow@C02Y13THJGH6:~:$ ```

[Patrick Massot]

I think those things were tested only on Debian-like systems. It would be very helpful to make them work on a fresh mac

[Jan-David Salchow]

That's my goal

[Jan-David Salchow]

Any idea why read doesn't work when piped through sh?

[Kevin Buzzard]

The update-mathlib thing: you are experiencing exactly what I experienced.

[Kevin Buzzard]

I was at AITP and random people were asking me how to install Lean and this is what I was faced with :-(

[Kevin Buzzard]

I had much better luck just cutting and pasting https://github.com/leanprover-community/mathlib/blob/master/scripts/remote-install-update-mathlib.sh into a file and running that.

[Kevin Buzzard]

Another thing that was awful: I made a new project with mathlib as a dependency, finally installed update-mathlib, and then it wouldn't work because it couldn't find olean files for that particular commit :-(

[Kevin Buzzard]

In the end I just got out my own laptop, looked at a commit which I knew update-mathlib would work for, memorised the first few characters of the commit hash, went back to their machine, cd'ed to _target/deps/mathlib, looked at the output of git log, found the commit, switched to that commit, and then manually edited the leanpkg.toml file to have that commit, and then finally it worked. Looked pretty slick ;-) not

[Jan-David Salchow]

read -p "update-mathlib needs to install python3 and pip3. Proceed?" -n 1 -r </dev/tty
solves that problem for me, the </dev/tty apparently tells read to use the terminal as an input

[Jan-David Salchow]

Ahh, https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh also uses </dev/tty

[Jan-David Salchow]

I've PRed this tiny change as #940 and tested it on my computer. I'm pretty sure it doesn't break anything that was working beforehand ;)

[Kevin Buzzard]

Thanks!

[Kevin Buzzard]

$ update-mathlib
  File "/home/buzzard/.mathlib/bin/update-mathlib", line 23
    os.system(f"curl {mathlib_url}/{branch}/{installer_path} -sSf | sh")
                                                                      ^
SyntaxError: invalid syntax
$

aargh [on Ubuntu 16.04]

[Kevin Buzzard]

Can I fix this easily? I'm out all day with a laptop and I don't fancy hammering my battery to compile mathlib.

[Kevin Buzzard]

Oh ok I figured how it all worked. I switched to a mathlib git commit from a couple of weeks ago and then ran the installer again which I found in scripts

[Jan-David Salchow]

I just wrote an explanation on why the fix is necessary, see https://github.com/leanprover-community/mathlib/pull/940#issuecomment-484211046

[Jan-David Salchow]

This makes me doubt that the fix is only required for Macs

[Jan-David Salchow]

I think all three reads should be broken, when executed as suggested above

[Jan-David Salchow]

Has anybody tried this on Debian without python installed?

[Ashwin Iyengar]

Hi! I'm trying to get started on macOS, and I followed the installation directions exactly as written on the github. Lean seems to be working fine in VSCode, but unfortunately after creating a new project with leanproject, running

import topology.basic
#check topological_space

(or any basic import really) results in loads of strange errors, none of which I understand at all. For instance it's complaining about syntax errors in tactic/alias.lean, and also docstrings starting with /-! or /-- result in lots of errors while docstrings starting with /- don't give any errors.

Are these kinds of things known problems, or have I just screwed something up?

[Kevin Buzzard]

Probably the latter. Did you "open folder" with VS Code? I never remember what the option looks like in a mac.

[Kevin Buzzard]

If you have a terminal, then change directory to the root directory of your project and type code . to open VS Code -- works in linux, not sure about mac.

[Kevin Buzzard]

But it's really important that you "open folder" and don't just open a file in your workspace directly with VS Code.

[Ashwin Iyengar]

Yeah I ran "leanproject new test-project" and then "code test-project" and opened the whole folder

[Kevin Buzzard]

Can you post the errors or send a screenshot?

[Kevin Buzzard]

Output of leanproject new test-project should be something like

$ leanproject new test-project
> mkdir -p test-project
> cd test-project
> mkdir src
> git init -q
> git checkout -b lean-3.4.2
Switched to a new branch 'lean-3.4.2'
configuring test-project 0.1
Adding mathlib
Looking for local mathlib oleans
Looking for remote mathlib oleans
Trying to download https://oleanstorage.azureedge.net/mathlib/6b095759061cbb736fdd7aaed8ca603a2e657b3e.tar.gz to /home/buzzard/.mathlib/6b095759061cbb736fdd7aaed8ca603a2e657b3e.tar.gz
100%|█████████████████████████████████████| 25.9M/25.9M [00:01<00:00, 22.5MiB/s]
Found mathlib oleans at https://oleanstorage.azureedge.net/mathlib/

[Kevin Buzzard]

After code test-project I navigate to src in VS Code, create a new file called test.lean and then after

import topology.basic
#check topological_space

I get

topological_space : Type u_1 → Type u_1

[Ashwin Iyengar]

Yeah so doing leanproject new test-project gives me

% leanproject new test-project
> cd test-project
> git init -q
> git checkout -b lean-3.9.0
Switched to a new branch 'lean-3.9.0'
configuring test-project 0.1
Adding mathlib
Looking for local mathlib oleans
Found local mathlib oleans

which looks about right

[Ashwin Iyengar]

one sec, I'll re-run the topology bit

[Kevin Buzzard]

Yes, this is the second time you did it so it found your oleans locally this time

[Kevin Buzzard]

The first time it will have downloaded them from a webserver.

[Kevin Buzzard]

WOOAH WOOAH WOOAH 3.9.0??

[Kevin Buzzard]

OK I know what the problem is :-)

[Ashwin Iyengar]

ahhh ok

[Kevin Buzzard]

and it's not your fault. We will have to fix it manually

[Ashwin Iyengar]

Kevin Buzzard said:

and it's not your fault. We will have to fix it manually

phew

[Kevin Buzzard]

The problem is that a few hours ago Lean got upgraded from 3.8.0 to 3.9.0, but the maths library didn't yet make the change

[Kevin Buzzard]

but I am a bit bewildered about how you managed to do this -- @Patrick Massot any idea? Wait, lemme upgrade leanproject so I'm in exactly the same mess as you.

[Ashwin Iyengar]

Ah wait, I think I did run elan update at some point to try to fix things (and it did download something new), but the bizarre errors that I'm getting were there before I ran elan update

[Kevin Buzzard]

Crap. How come my leanproject is doing the right thing? What happens if you type leanproject --version?

[Ashwin Iyengar]

leanproject, version 0.0.5

[Kevin Buzzard]

OK and if you just completely start again with leanproject new test-project you get 3.9.0?

[Ashwin Iyengar]

yep

[Kevin Buzzard]

Anyway, let's just fix it. Sorry about this, you caught us at a bad moment.

[Kevin Buzzard]

Go into the root directory of your project and tell me the contents of leanpkg.toml

[Ashwin Iyengar]

[package]
name = "test-project"
version = "0.1"
lean_version = "leanprover-community/lean:3.8.0"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "6b095759061cbb736fdd7aaed8ca603a2e657b3e"}

[Kevin Buzzard]

oh, that's exactly what it should say.

[Kevin Buzzard]

Then I am back to being confused. I was going to tell you to change it to that.

[Ashwin Iyengar]

yeah strange that it says 3.8.0 after installing 3.9.0...

[Kevin Buzzard]

Still in the root directory of your project, type lean --make _target/deps/mathlib/src/data/real/basic.lean

[Kevin Buzzard]

You should get no output and the compilation should take no more than a few seconds.

[Ashwin Iyengar]

yep no output, ran quickly

[Kevin Buzzard]

OK great. So you have got a fully installed Lean and mathlib. Oh, while we're here, try lean --version.

[Kevin Buzzard]

You should be on 3.8.0

[Ashwin Iyengar]

Lean (version 3.8.0, commit e694f496aa08, Release)

[Kevin Buzzard]

You did everything right.

[Ashwin Iyengar]

Maybe it's an issue with VSCode?

[Kevin Buzzard]

That's all that is left.

[Kevin Buzzard]

So open up VS Code, stick a file called test.lean in the src directory of your project and try what you tried before:

import topology.basic
#check topological_space

[Kevin Buzzard]

and if clicking on #check doesn't give you topological_space : Type u_1 → Type u_1 then send a screenshot (you can do it with the paper clip just under the box where you type assuming you're using a computer)

[Ashwin Iyengar]

Yeah so if I run lean src/test.lean from the command line everything works and it outputs topological_space : Type u_1 → Type u_1

[Ashwin Iyengar]

One sec, I'll see what VSCode says (takes a while to parse...)

[Kevin Buzzard]

That's because you got everything set up correctly :-)

[Mario Carneiro]

you can also #print lean.version from vscode

[Kevin Buzzard]

I am still bewildered by the way. The whole 3.9.0 thing was a complete red herring. It sounds like you've done everything perfectly and the new bump to Lean 3.9.0 didn't mess anything up at all.

[Kevin Buzzard]

lean.version : ℕ × ℕ × ℕ

[Kevin Buzzard]

Mario did you just troll me?

[Kevin Buzzard]

oh rofl

[Kevin Buzzard]

that's the result of #check lean.version :laughing:

[Mario Carneiro]

does #eval work?

[Ashwin Iyengar]

haha yeah I got the same thing

[Kevin Buzzard]

(3, (8, 0))

[Ashwin Iyengar]

if i run #print lean.version i get def lean.version : ℕ × ℕ × ℕ := (3, 4, 2)

[Mario Carneiro]

I will recommend that in the future then

[Mario Carneiro]

okay that's not good

[Kevin Buzzard]

Aah OK so there's your problem Ashwin, Lean is running 3.4.2 in VS Code but you're set up to run 3.8.0

[Ashwin Iyengar]

yes that makes sense... i'll see if I can find it in the VSCode settings somewhere i guess

[Kevin Buzzard]

Did you screw with VS Code settings at some point?

[Kevin Buzzard]

You already confessed that you screwed with elan

[Ashwin Iyengar]

Nope elan is the only thing I dared mess with

[Mario Carneiro]

VS Code is also set up to use lean by default so it depends on your PATH what exactly that resolves to

[Mario Carneiro]

what do you get from lean --version at the vscode console

[Kevin Buzzard]

You can get the console by dragging up from the top line of the blue bar at the bottom of VS Code.

[Ashwin Iyengar]

ash@MacBook-Pro-3 test-project % lean --version Lean (version 3.8.0, commit e694f496aa08, Release)

[Kevin Buzzard]

OK so in VS Code try File -> Preferences -> Settings

[Kevin Buzzard]

and then search for lean

[Kevin Buzzard]

and what is in the box for Lean : Executable Path?

[Ashwin Iyengar]

Oh "/Applications/Lean/lean-3.4.2-darwin/bin/lean"

[Kevin Buzzard]

Aah :-)

[Ashwin Iyengar]

I guess i must have installed lean at some point last year?

[Kevin Buzzard]

There's the culprit

[Kevin Buzzard]

Just remove it completely, leave the box blank

[Kevin Buzzard]

and then Ctrl-Shift-P and then type "restart lean" in the box and select the option which appears

[Kevin Buzzard]

Sorry, it's "Lean : restart"

[Ashwin Iyengar]

yay! it works now

[Ashwin Iyengar]

thanks Kevin!

[Kevin Buzzard]

A couple of years ago I think there was a good reason to be typing stuff into that box

[Kevin Buzzard]

but since then the community has made a huge effort to make everything work out of the box

[Kevin Buzzard]

so anything in the box is a bad idea

[Kevin Buzzard]

Now go do maths :-)

[Ashwin Iyengar]

yeah i was impressed by how smooth the installation process is generally

[Kevin Buzzard]

That was a pretty impressive gotcha.

[Kevin Buzzard]

@Patrick Massot can you explain why whenever someone types leanproject new blah a version of lean is mentioned which never seems to be the version a user ends up with? :-)

[Reid Barton]

Pretty smooth aside from that brief moment when you slipped into the future

[Ashwin Iyengar]

well if I run lean --version inside the project folder it tells me 3.8.0 but if i run it outside the folder it tells me 3.9.0

[Kevin Buzzard]

That makes sense

[Kevin Buzzard]

The lean program decides which version of Lean to use by looking for a leanpkg.toml

[Kevin Buzzard]

that was why that was the first question I asked

[Scott Morrison]

Can we now change the VS Code extension to not even give people the option of putting something in that box? It seems the hold-outs who won't use elan can probably be left to fend for themselves, and we'll save a lot of trouble.

[Bryan Gin-ge Chen]

I'd prefer adding a stern warning there instead of taking the setting away entirely. If I recall correctly, Patrick's portable VS Code experiment relied on that setting.

[Mario Carneiro]

I think that having the setting is important. Sometimes the automatic tools don't work, for whatever reason, and I don't want to rely too deeply on their presence

[Scott Morrison]

Perhaps then just a warning on it. "Do not use this setting unless you are a Mario-level expert user!" :-)

[Johan Commelin]

Why is there no :mario: emoji?

[Bryan Gin-ge Chen]

Warnings PR'd: https://github.com/leanprover/vscode-lean/pull/156 (No Mario references, sorry...)

[Mario Carneiro]

Did you know zulip lets you add custom emoji? I'm glad no one has noticed yet because it sounds easy to abuse

[Mario Carneiro]

oh wait, it's an admin only feature. that makes me feel slightly better about it

[Johan Commelin]

image.png

[Patrick Massot]

We need a version of this image adding Mario's beard.

[Chris M]

@Bryan Gin-ge Chen , if I run that in git bash, I get "invalid git repository".

I realized: perhaps I haven't actually installed Lean correctly a while back (I've had Lean on VSCode for a while now, not using it for a few months). So I tried reinstalling based on the description in https://leanprover-community.github.io/install/windows.html. But after entering the command curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh, I get the error error: could not remove 'elan-bin' file: 'C:\Users\chris\.elan\bin\elan.exe' info: caused by: Access is denied. (os error 5)

What should I do about this?

[Bryan Gin-ge Chen]

That means you already have elan installed. You can update elan by typing elan self update.

[Bryan Gin-ge Chen]

What do you see if you type leanproject --version? The latest version is 0.0.8. If you don't have that version, you should be able to upgrade with pip install --upgrade mathlibtools.

[Chris M]

If I write elan self update I still get error: could not remove 'elan-bin' file: 'C:\Users\chris\.elan\bin\elan.exe' info: caused by: Access is denied. (os error 5).

leanproject --version gave me version 0.0.5, and after the update I have 0.0.8. However, after trying elan self update after that, I got the same error.

[Bryan Gin-ge Chen]

I'm not sure how permissions in Windows work, but you should try and see if you can change the permissions of everything in C:\Users\chris\.elan. It might be easier just to delete that directory entirely and try reinstalling it.

By the way, leanproject and elan are separate tools (though leanproject makes use of elan), so there's no reason to expect that upgrading leanproject would fix elan.

[Bryan Gin-ge Chen]

Anyways, I'm not sure what could be causing "invalid git repository".

[Chris M]

It turned out to be very simple. I had to close VSCode

[Chris M]

Ok I have managed to get it to work. It turned out I didn't create a lean project but instead just had separate .lean files, and hence didn't have access to the mathlib library