Zulip Chat Archive

Stream: new members

Topic: Installing mathlib


view this post on Zulip Jasmin Blanchette (Apr 05 2019 at 07:34):

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.

view this post on Zulip Johan Commelin (Apr 05 2019 at 07:35):

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

view this post on Zulip Patrick Massot (Apr 05 2019 at 07:35):

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

view this post on Zulip Patrick Massot (Apr 05 2019 at 07:36):

But you can do it if you insist

view this post on Zulip Jasmin Blanchette (Apr 05 2019 at 07:36):

I can create a project.

view this post on Zulip Jasmin Blanchette (Apr 05 2019 at 07:36):

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

view this post on Zulip Patrick Massot (Apr 05 2019 at 07:40):

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

view this post on Zulip Patrick Massot (Apr 05 2019 at 07:41):

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

view this post on Zulip Patrick Massot (Apr 05 2019 at 07:41):

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

view this post on Zulip Patrick Massot (Apr 05 2019 at 07:42):

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...

view this post on Zulip Johan Commelin (Apr 05 2019 at 07:43):

Does leanpkg default to lean version 3.4.2 nowadays?

view this post on Zulip Johan Commelin (Apr 05 2019 at 07:44):

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.

view this post on Zulip Patrick Massot (Apr 05 2019 at 07:45):

Johan, please don't make things sound complicated

view this post on Zulip Patrick Massot (Apr 05 2019 at 07:45):

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

view this post on Zulip Jasmin Blanchette (Apr 05 2019 at 07:47):

I've used elan with default answers.

view this post on Zulip Johan Commelin (Apr 05 2019 at 07:47):

Last week things weren't fine when I helped Fabian

view this post on Zulip Jasmin Blanchette (Apr 05 2019 at 07:47):

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

view this post on Zulip Jasmin Blanchette (Apr 05 2019 at 07:48):

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

view this post on Zulip Patrick Massot (Apr 05 2019 at 07:48):

That .lean is indeed used for lean files outside projects

view this post on Zulip Jasmin Blanchette (Apr 05 2019 at 07:48):

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

view this post on Zulip Patrick Massot (Apr 05 2019 at 07:49):

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

view this post on Zulip Jasmin Blanchette (Apr 05 2019 at 07:49):

Hm... now I'm confused

view this post on Zulip Jasmin Blanchette (Apr 05 2019 at 07:49):

I think I'll ask Johannes.

view this post on Zulip Patrick Massot (Apr 05 2019 at 07:49):

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

view this post on Zulip Patrick Massot (Apr 05 2019 at 07:50):

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

view this post on Zulip Jasmin Blanchette (Apr 05 2019 at 07:51):

OK let me try.

view this post on Zulip Jasmin Blanchette (Apr 05 2019 at 07:51):

You mean 1+ 4 lines, right?

view this post on Zulip Patrick Massot (Apr 05 2019 at 07:52):

yes

view this post on Zulip Jasmin Blanchette (Apr 05 2019 at 07:54):

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

view this post on Zulip Jasmin Blanchette (Apr 05 2019 at 07:54):

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

view this post on Zulip Jasmin Blanchette (Apr 05 2019 at 07:55):

with Johannes's approach it didn't

view this post on Zulip Jasmin Blanchette (Apr 05 2019 at 07:55):

which means I could freely use mathlib anywhere no questions asked

view this post on Zulip Jasmin Blanchette (Apr 05 2019 at 07:55):

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

view this post on Zulip Jasmin Blanchette (Apr 05 2019 at 07:56):

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

view this post on Zulip Patrick Massot (Apr 05 2019 at 07:58):

Did you source .profile after installing update-mathlib?

view this post on Zulip Patrick Massot (Apr 05 2019 at 07:59):

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

view this post on Zulip Jasmin Blanchette (Apr 05 2019 at 07:59):

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

view this post on Zulip Patrick Massot (Apr 05 2019 at 08:00):

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

view this post on Zulip Patrick Massot (Apr 05 2019 at 08:01):

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

view this post on Zulip Jasmin Blanchette (Apr 05 2019 at 08:01):

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

view this post on Zulip Jasmin Blanchette (Apr 05 2019 at 08:02):

It seems like .lean gets read automatically or something.

view this post on Zulip Patrick Massot (Apr 05 2019 at 08:03):

only if you are outside of all projects

view this post on Zulip Jasmin Blanchette (Apr 05 2019 at 08:03):

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

view this post on Zulip Jasmin Blanchette (Apr 05 2019 at 08:04):

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

view this post on Zulip Patrick Massot (Apr 05 2019 at 08:05):

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

view this post on Zulip Jasmin Blanchette (Apr 05 2019 at 08:31):

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

view this post on Zulip Jasmin Blanchette (Apr 05 2019 at 08:31):

but that's in November

view this post on Zulip Jasmin Blanchette (Apr 05 2019 at 08:32):

and students will have to create homework etc.

view this post on Zulip Jasmin Blanchette (Apr 05 2019 at 08:32):

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

view this post on Zulip Jasmin Blanchette (Apr 05 2019 at 08:33):

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

view this post on Zulip Jasmin Blanchette (Apr 05 2019 at 08:34):

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

view this post on Zulip Johannes Hölzl (Apr 05 2019 at 17:45):

didn't we use leanpkg install ...?

view this post on Zulip Jan-David Salchow (Apr 15 2019 at 20:12):

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

view this post on Zulip Jan-David Salchow (Apr 15 2019 at 20:12):

The first step doesn't

view this post on Zulip Jan-David Salchow (Apr 15 2019 at 20:12):

there is brew on the computer, but no python

view this post on Zulip Jan-David Salchow (Apr 15 2019 at 20:13):

So read should ask me if I want to install python3

view this post on Zulip Kevin Buzzard (Apr 15 2019 at 20:13):

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.

view this post on Zulip Jan-David Salchow (Apr 15 2019 at 20:14):

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:~:$ ```

view this post on Zulip Patrick Massot (Apr 15 2019 at 20:15):

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

view this post on Zulip Jan-David Salchow (Apr 15 2019 at 20:16):

That's my goal

view this post on Zulip Jan-David Salchow (Apr 15 2019 at 20:16):

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

view this post on Zulip Kevin Buzzard (Apr 15 2019 at 20:16):

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

view this post on Zulip Kevin Buzzard (Apr 15 2019 at 20:17):

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

view this post on Zulip Kevin Buzzard (Apr 15 2019 at 20:17):

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.

view this post on Zulip Kevin Buzzard (Apr 15 2019 at 20:18):

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 :-(

view this post on Zulip Kevin Buzzard (Apr 15 2019 at 20:19):

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

view this post on Zulip Jan-David Salchow (Apr 15 2019 at 20:44):

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

view this post on Zulip Jan-David Salchow (Apr 15 2019 at 20:49):

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

view this post on Zulip Jan-David Salchow (Apr 15 2019 at 21:24):

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 ;)

view this post on Zulip Kevin Buzzard (Apr 15 2019 at 21:24):

Thanks!

view this post on Zulip Kevin Buzzard (Apr 16 2019 at 10:37):

$ 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]

view this post on Zulip Kevin Buzzard (Apr 16 2019 at 10:59):

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

view this post on Zulip Kevin Buzzard (Apr 16 2019 at 11:24):

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

view this post on Zulip Jan-David Salchow (Apr 17 2019 at 18:37):

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

view this post on Zulip Jan-David Salchow (Apr 17 2019 at 18:38):

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

view this post on Zulip Jan-David Salchow (Apr 17 2019 at 18:39):

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

view this post on Zulip Jan-David Salchow (Apr 17 2019 at 18:42):

Has anybody tried this on Debian without python installed?

view this post on Zulip Ashwin Iyengar (Apr 18 2020 at 23:32):

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?

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:34):

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

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:34):

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.

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:35):

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

view this post on Zulip Ashwin Iyengar (Apr 18 2020 at 23:35):

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

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:36):

Can you post the errors or send a screenshot?

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:37):

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/

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:38):

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

view this post on Zulip Ashwin Iyengar (Apr 18 2020 at 23:39):

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

view this post on Zulip Ashwin Iyengar (Apr 18 2020 at 23:39):

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

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:39):

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

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:40):

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

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:40):

WOOAH WOOAH WOOAH 3.9.0??

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:40):

OK I know what the problem is :-)

view this post on Zulip Ashwin Iyengar (Apr 18 2020 at 23:40):

ahhh ok

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:40):

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

view this post on Zulip Ashwin Iyengar (Apr 18 2020 at 23:41):

Kevin Buzzard said:

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

phew

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:41):

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

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:42):

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.

view this post on Zulip Ashwin Iyengar (Apr 18 2020 at 23:43):

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

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:43):

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

view this post on Zulip Ashwin Iyengar (Apr 18 2020 at 23:44):

leanproject, version 0.0.5

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:44):

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

view this post on Zulip Ashwin Iyengar (Apr 18 2020 at 23:44):

yep

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:44):

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

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:45):

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

view this post on Zulip Ashwin Iyengar (Apr 18 2020 at 23:45):

[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"}

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:46):

oh, that's exactly what it should say.

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:46):

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

view this post on Zulip Ashwin Iyengar (Apr 18 2020 at 23:46):

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

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:47):

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

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:47):

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

view this post on Zulip Ashwin Iyengar (Apr 18 2020 at 23:48):

yep no output, ran quickly

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:48):

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

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:49):

You should be on 3.8.0

view this post on Zulip Ashwin Iyengar (Apr 18 2020 at 23:49):

Lean (version 3.8.0, commit e694f496aa08, Release)

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:49):

You did everything right.

view this post on Zulip Ashwin Iyengar (Apr 18 2020 at 23:49):

Maybe it's an issue with VSCode?

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:49):

That's all that is left.

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:50):

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

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:51):

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)

view this post on Zulip Ashwin Iyengar (Apr 18 2020 at 23:51):

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

view this post on Zulip Ashwin Iyengar (Apr 18 2020 at 23:51):

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

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:51):

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

view this post on Zulip Mario Carneiro (Apr 18 2020 at 23:52):

you can also #print lean.version from vscode

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:52):

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.

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:53):

lean.version : ℕ × ℕ × ℕ

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:53):

Mario did you just troll me?

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:53):

oh rofl

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:53):

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

view this post on Zulip Mario Carneiro (Apr 18 2020 at 23:54):

does #eval work?

view this post on Zulip Ashwin Iyengar (Apr 18 2020 at 23:54):

haha yeah I got the same thing

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:54):

(3, (8, 0))

view this post on Zulip Ashwin Iyengar (Apr 18 2020 at 23:54):

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

view this post on Zulip Mario Carneiro (Apr 18 2020 at 23:54):

I will recommend that in the future then

view this post on Zulip Mario Carneiro (Apr 18 2020 at 23:55):

okay that's not good

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:55):

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

view this post on Zulip Ashwin Iyengar (Apr 18 2020 at 23:55):

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

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:55):

Did you screw with VS Code settings at some point?

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:55):

You already confessed that you screwed with elan

view this post on Zulip Ashwin Iyengar (Apr 18 2020 at 23:56):

Nope elan is the only thing I dared mess with

view this post on Zulip Mario Carneiro (Apr 18 2020 at 23:56):

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

view this post on Zulip Mario Carneiro (Apr 18 2020 at 23:57):

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

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:57):

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

view this post on Zulip Ashwin Iyengar (Apr 18 2020 at 23:57):

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

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:57):

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

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:58):

and then search for lean

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:58):

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

view this post on Zulip Ashwin Iyengar (Apr 18 2020 at 23:58):

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

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:58):

Aah :-)

view this post on Zulip Ashwin Iyengar (Apr 18 2020 at 23:58):

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

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:59):

There's the culprit

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:59):

Just remove it completely, leave the box blank

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 23:59):

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

view this post on Zulip Kevin Buzzard (Apr 19 2020 at 00:00):

Sorry, it's "Lean : restart"

view this post on Zulip Ashwin Iyengar (Apr 19 2020 at 00:00):

yay! it works now

view this post on Zulip Ashwin Iyengar (Apr 19 2020 at 00:00):

thanks Kevin!

view this post on Zulip Kevin Buzzard (Apr 19 2020 at 00:00):

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

view this post on Zulip Kevin Buzzard (Apr 19 2020 at 00:00):

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

view this post on Zulip Kevin Buzzard (Apr 19 2020 at 00:00):

so anything in the box is a bad idea

view this post on Zulip Kevin Buzzard (Apr 19 2020 at 00:01):

Now go do maths :-)

view this post on Zulip Ashwin Iyengar (Apr 19 2020 at 00:01):

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

view this post on Zulip Kevin Buzzard (Apr 19 2020 at 00:02):

That was a pretty impressive gotcha.

view this post on Zulip Kevin Buzzard (Apr 19 2020 at 00:02):

@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? :-)

view this post on Zulip Reid Barton (Apr 19 2020 at 00:03):

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

view this post on Zulip Ashwin Iyengar (Apr 19 2020 at 00:04):

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

view this post on Zulip Kevin Buzzard (Apr 19 2020 at 00:04):

That makes sense

view this post on Zulip Kevin Buzzard (Apr 19 2020 at 00:04):

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

view this post on Zulip Kevin Buzzard (Apr 19 2020 at 00:04):

that was why that was the first question I asked

view this post on Zulip Scott Morrison (Apr 19 2020 at 00:07):

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.

view this post on Zulip Bryan Gin-ge Chen (Apr 19 2020 at 02:03):

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.

view this post on Zulip Mario Carneiro (Apr 19 2020 at 02:19):

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

view this post on Zulip Scott Morrison (Apr 19 2020 at 02:39):

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

view this post on Zulip Johan Commelin (Apr 19 2020 at 06:10):

Why is there no :mario: emoji?

view this post on Zulip Bryan Gin-ge Chen (Apr 19 2020 at 06:16):

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

view this post on Zulip Mario Carneiro (Apr 19 2020 at 07:08):

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

view this post on Zulip Mario Carneiro (Apr 19 2020 at 07:10):

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

view this post on Zulip Johan Commelin (Apr 19 2020 at 07:11):

image.png

view this post on Zulip Patrick Massot (Apr 19 2020 at 10:10):

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

view this post on Zulip Chris M (Jun 29 2020 at 08:56):

@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?

view this post on Zulip Bryan Gin-ge Chen (Jun 29 2020 at 08:57):

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

view this post on Zulip Bryan Gin-ge Chen (Jun 29 2020 at 09:00):

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.

view this post on Zulip Chris M (Jun 29 2020 at 09:04):

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.

view this post on Zulip Bryan Gin-ge Chen (Jun 29 2020 at 09:07):

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.

view this post on Zulip Bryan Gin-ge Chen (Jun 29 2020 at 09:09):

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

view this post on Zulip Chris M (Jun 29 2020 at 09:10):

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

view this post on Zulip Chris M (Jun 29 2020 at 09:22):

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


Last updated: May 15 2021 at 23:13 UTC