Zulip Chat Archive

Stream: new members

Topic: Installing mathlib


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.

Johan Commelin (Apr 05 2019 at 07:35):

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

Patrick Massot (Apr 05 2019 at 07:35):

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

Patrick Massot (Apr 05 2019 at 07:36):

But you can do it if you insist

Jasmin Blanchette (Apr 05 2019 at 07:36):

I can create a project.

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.

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

Patrick Massot (Apr 05 2019 at 07:41):

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

Patrick Massot (Apr 05 2019 at 07:41):

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

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

Johan Commelin (Apr 05 2019 at 07:43):

Does leanpkg default to lean version 3.4.2 nowadays?

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.

Patrick Massot (Apr 05 2019 at 07:45):

Johan, please don't make things sound complicated

Patrick Massot (Apr 05 2019 at 07:45):

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

Jasmin Blanchette (Apr 05 2019 at 07:47):

I've used elan with default answers.

Johan Commelin (Apr 05 2019 at 07:47):

Last week things weren't fine when I helped Fabian

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.

Jasmin Blanchette (Apr 05 2019 at 07:48):

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

Patrick Massot (Apr 05 2019 at 07:48):

That .lean is indeed used for lean files outside projects

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.

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

Jasmin Blanchette (Apr 05 2019 at 07:49):

Hm... now I'm confused

Jasmin Blanchette (Apr 05 2019 at 07:49):

I think I'll ask Johannes.

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.

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

Jasmin Blanchette (Apr 05 2019 at 07:51):

OK let me try.

Jasmin Blanchette (Apr 05 2019 at 07:51):

You mean 1+ 4 lines, right?

Patrick Massot (Apr 05 2019 at 07:52):

yes

Jasmin Blanchette (Apr 05 2019 at 07:54):

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

Jasmin Blanchette (Apr 05 2019 at 07:54):

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

Jasmin Blanchette (Apr 05 2019 at 07:55):

with Johannes's approach it didn't

Jasmin Blanchette (Apr 05 2019 at 07:55):

which means I could freely use mathlib anywhere no questions asked

Jasmin Blanchette (Apr 05 2019 at 07:55):

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

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.

Patrick Massot (Apr 05 2019 at 07:58):

Did you source .profile after installing update-mathlib?

Patrick Massot (Apr 05 2019 at 07:59):

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

Jasmin Blanchette (Apr 05 2019 at 07:59):

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

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

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

Jasmin Blanchette (Apr 05 2019 at 08:01):

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

Jasmin Blanchette (Apr 05 2019 at 08:02):

It seems like .lean gets read automatically or something.

Patrick Massot (Apr 05 2019 at 08:03):

only if you are outside of all projects

Jasmin Blanchette (Apr 05 2019 at 08:03):

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

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

Patrick Massot (Apr 05 2019 at 08:05):

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

Jasmin Blanchette (Apr 05 2019 at 08:31):

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

Jasmin Blanchette (Apr 05 2019 at 08:31):

but that's in November

Jasmin Blanchette (Apr 05 2019 at 08:32):

and students will have to create homework etc.

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

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

Jasmin Blanchette (Apr 05 2019 at 08:34):

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

Johannes Hölzl (Apr 05 2019 at 17:45):

didn't we use leanpkg install ...?

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

Jan-David Salchow (Apr 15 2019 at 20:12):

The first step doesn't

Jan-David Salchow (Apr 15 2019 at 20:12):

there is brew on the computer, but no python

Jan-David Salchow (Apr 15 2019 at 20:13):

So read should ask me if I want to install python3

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.

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

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

Jan-David Salchow (Apr 15 2019 at 20:16):

That's my goal

Jan-David Salchow (Apr 15 2019 at 20:16):

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

Kevin Buzzard (Apr 15 2019 at 20:16):

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

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

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.

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

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

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

Jan-David Salchow (Apr 15 2019 at 20:49):

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

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

Kevin Buzzard (Apr 15 2019 at 21:24):

Thanks!

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]

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.

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

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

Jan-David Salchow (Apr 17 2019 at 18:38):

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

Jan-David Salchow (Apr 17 2019 at 18:39):

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

Jan-David Salchow (Apr 17 2019 at 18:42):

Has anybody tried this on Debian without python installed?

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?

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.

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.

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.

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

Kevin Buzzard (Apr 18 2020 at 23:36):

Can you post the errors or send a screenshot?

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/

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

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

Ashwin Iyengar (Apr 18 2020 at 23:39):

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

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

Kevin Buzzard (Apr 18 2020 at 23:40):

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

Kevin Buzzard (Apr 18 2020 at 23:40):

WOOAH WOOAH WOOAH 3.9.0??

Kevin Buzzard (Apr 18 2020 at 23:40):

OK I know what the problem is :-)

Ashwin Iyengar (Apr 18 2020 at 23:40):

ahhh ok

Kevin Buzzard (Apr 18 2020 at 23:40):

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

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

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

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.

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

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?

Ashwin Iyengar (Apr 18 2020 at 23:44):

leanproject, version 0.0.5

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?

Ashwin Iyengar (Apr 18 2020 at 23:44):

yep

Kevin Buzzard (Apr 18 2020 at 23:44):

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

Kevin Buzzard (Apr 18 2020 at 23:45):

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

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

Kevin Buzzard (Apr 18 2020 at 23:46):

oh, that's exactly what it should say.

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.

Ashwin Iyengar (Apr 18 2020 at 23:46):

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

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

Kevin Buzzard (Apr 18 2020 at 23:47):

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

Ashwin Iyengar (Apr 18 2020 at 23:48):

yep no output, ran quickly

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.

Kevin Buzzard (Apr 18 2020 at 23:49):

You should be on 3.8.0

Ashwin Iyengar (Apr 18 2020 at 23:49):

Lean (version 3.8.0, commit e694f496aa08, Release)

Kevin Buzzard (Apr 18 2020 at 23:49):

You did everything right.

Ashwin Iyengar (Apr 18 2020 at 23:49):

Maybe it's an issue with VSCode?

Kevin Buzzard (Apr 18 2020 at 23:49):

That's all that is left.

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

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)

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

Ashwin Iyengar (Apr 18 2020 at 23:51):

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

Kevin Buzzard (Apr 18 2020 at 23:51):

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

Mario Carneiro (Apr 18 2020 at 23:52):

you can also #print lean.version from vscode

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.

Kevin Buzzard (Apr 18 2020 at 23:53):

lean.version : ℕ × ℕ × ℕ

Kevin Buzzard (Apr 18 2020 at 23:53):

Mario did you just troll me?

Kevin Buzzard (Apr 18 2020 at 23:53):

oh rofl

Kevin Buzzard (Apr 18 2020 at 23:53):

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

Mario Carneiro (Apr 18 2020 at 23:54):

does #eval work?

Ashwin Iyengar (Apr 18 2020 at 23:54):

haha yeah I got the same thing

Kevin Buzzard (Apr 18 2020 at 23:54):

(3, (8, 0))

Ashwin Iyengar (Apr 18 2020 at 23:54):

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

Mario Carneiro (Apr 18 2020 at 23:54):

I will recommend that in the future then

Mario Carneiro (Apr 18 2020 at 23:55):

okay that's not good

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

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

Kevin Buzzard (Apr 18 2020 at 23:55):

Did you screw with VS Code settings at some point?

Kevin Buzzard (Apr 18 2020 at 23:55):

You already confessed that you screwed with elan

Ashwin Iyengar (Apr 18 2020 at 23:56):

Nope elan is the only thing I dared mess with

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

Mario Carneiro (Apr 18 2020 at 23:57):

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

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.

Ashwin Iyengar (Apr 18 2020 at 23:57):

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

Kevin Buzzard (Apr 18 2020 at 23:57):

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

Kevin Buzzard (Apr 18 2020 at 23:58):

and then search for lean

Kevin Buzzard (Apr 18 2020 at 23:58):

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

Ashwin Iyengar (Apr 18 2020 at 23:58):

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

Kevin Buzzard (Apr 18 2020 at 23:58):

Aah :-)

Ashwin Iyengar (Apr 18 2020 at 23:58):

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

Kevin Buzzard (Apr 18 2020 at 23:59):

There's the culprit

Kevin Buzzard (Apr 18 2020 at 23:59):

Just remove it completely, leave the box blank

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

Kevin Buzzard (Apr 19 2020 at 00:00):

Sorry, it's "Lean : restart"

Ashwin Iyengar (Apr 19 2020 at 00:00):

yay! it works now

Ashwin Iyengar (Apr 19 2020 at 00:00):

thanks Kevin!

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

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

Kevin Buzzard (Apr 19 2020 at 00:00):

so anything in the box is a bad idea

Kevin Buzzard (Apr 19 2020 at 00:01):

Now go do maths :-)

Ashwin Iyengar (Apr 19 2020 at 00:01):

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

Kevin Buzzard (Apr 19 2020 at 00:02):

That was a pretty impressive gotcha.

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

Reid Barton (Apr 19 2020 at 00:03):

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

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

Kevin Buzzard (Apr 19 2020 at 00:04):

That makes sense

Kevin Buzzard (Apr 19 2020 at 00:04):

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

Kevin Buzzard (Apr 19 2020 at 00:04):

that was why that was the first question I asked

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.

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.

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

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!" :-)

Johan Commelin (Apr 19 2020 at 06:10):

Why is there no :mario: emoji?

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

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

Mario Carneiro (Apr 19 2020 at 07:10):

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

Johan Commelin (Apr 19 2020 at 07:11):

image.png

Patrick Massot (Apr 19 2020 at 10:10):

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

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?

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.

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.

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.

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.

Bryan Gin-ge Chen (Jun 29 2020 at 09:09):

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

Chris M (Jun 29 2020 at 09:10):

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

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: Dec 20 2023 at 11:08 UTC