install session

Stream: Lean for the curious mathematician 2020

[Johan Commelin]

Hello everyone! Welcome to this conference. The official programs starts at 13:00 (UTC+2). This morning session is devoted to installing Lean, and debugging any problems that might arise.
Please see the following youtube playlist for installation instructions and some other "getting started" videos: https://www.youtube.com/playlist?list=PLlF-CfQhukNnxF1S22cNGKyfOrd380NUv
If you have any problems, you can ask them here on Zulip.

[Patrick Massot]

GitHub seems to have trouble this morning...

[Johan Commelin]

Yup... we just noticed.

[Patrick Massot]

https://www.githubstatus.com/ tells us that GitHub is indeed misbehaving but should respond to git commands. Hopefully this means you can still install everything but may have trouble navigating some web pages. We're sorry for the inconvenience.

[Filippo A. E. Nuccio]

I was trying to re-download the tutorials, but I get the error
leanproject get tutorials Cloning from https://github.com/leanprover-community/tutorials.git Command '['leanpkg', 'configure']' returned non-zero exit status 1.

[Patrick Massot]

It works here.

[Patrick Massot]

But it's the nature of GitHub glitches that things are not reproducible.

[Scott Morrison]

You should try running the underlying git command.

[Scott Morrison]

...

[Scott Morrison]

git clone https://github.com/leanprover-community/tutorials.git

[Patrick Massot]

That won't change anything. leanproject runs it for you without doing anything fancy at this stage.

[Filippo A. E. Nuccio]

Well, but it has actually worked.

[Johan Commelin]

That must have been quantum luck :oops: :grinning_face_with_smiling_eyes:

[Filippo A. E. Nuccio]

I have performed a git pull on mathlib but now VSCode is always orange, like compiling the whole mathlib locally on my pc. I have tried to do leanproject get-mathlib-cache but I get an error (Failed to fetch mathlib oleans Info: No github section found in 'git config', we will use GitHub with no authentication)

[Johan Commelin]

ls _target/deps/mathlib/src/data/*.olean should show a non-empty list of files

[Johan Commelin]

I'm afraid that github did not give you that mathlib cache

[Johan Commelin]

The Info piece is innocent. It should work nevertheless.

[Anne Baanen]

Hey @Filippo A. E. Nuccio, nice to see you again :) I think your mathlib may be pulling from your fork instead of leanprover-community/mathlib.

[Filippo A. E. Nuccio]

ANd with ls I get
ls: cannot access '_target/deps/mathlib/src/data/*.olean': No such file or directory

[Filippo A. E. Nuccio]

Hey @Anne Baanen , nice to see you!

[Filippo A. E. Nuccio]

AH! I always get git wrong...

[Anne Baanen]

I think we can check with git branch -vv where git pull will look by default

[Filippo A. E. Nuccio]

* Vierkantor-dedekind-domain 9482cd9bf Set-up strategy for Samuel's proof master 41e699455 [origin/master] Merge branch 'master' of https://github.com/faenuccio/mathlib

[Patrick Massot]

Are you screen sharing on Zoom?

[Filippo A. E. Nuccio]

Right, I was pulling from my fork, if I understand the last line correctly

[Filippo A. E. Nuccio]

I will

[Anne Baanen]

I will join Zoom shortly, once I have run a few errands

[Filippo A. E. Nuccio]

Now I'm on Zoom, can share my screen

[Luuk Stehouwer]

I'm trying to install elan using https://leanprover-community.github.io/install/macos_details.html. I have to run
curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh
but GitHub gives me a 500. Can I get elan in a different way?

[Johan Commelin]

Unfortunately github seems to have problems this morning https://www.githubstatus.com/

[Johan Commelin]

I don't think we have another way to get elan at the moment. I'm very sorry for the trouble.

[Luuk Stehouwer]

:oh_no:

[Luuk Stehouwer]

OK thanks

[Pim Spelier]

Is elan necessary to get lean to work? (I have the same problem as Luuk)

[Scott Morrison]

elan is not strictly speaking necessary

[Scott Morrison]

but you'll be compiling Lean from scratch, which is more than we can manage helping with this morning. :-)

[Gabriel Ebner]

Github seems to be up again.

[Johan Commelin]

Wow, I hope so!

[Scott Morrison]

Working for me!

[Patrick Massot]

The githubstatus website is less optimistic

[Luuk Stehouwer]

Installing elan works for me

[Johan Commelin]

Great! I'm really happy now

[Sophie Morel]

And I was able to add my SSH key to my github account. :)

[Sophie Morel]

Now the 'leanproject get tutorials' command is running as expected on my macbook too.

[Daan van Gent]

I get "
Cloning from https://github.com/leanprover-community/tutorials.git
[Errno 2] No such file or directory: 'leanpkg': 'leanpkg'
"
does that mean my lean install failed?

[Johan Commelin]

Yup... something must have gone wrong with the elan part of the install

[Johan Commelin]

Which system are you on?

[Daan van Gent]

Ubuntu

[Johan Commelin]

Ok... did you add the elan directory to your path?

[Daan van Gent]

I did nothing more than run the installation oneliner in the youtube video

[Johan Commelin]

Hmm... strange. Anything special about your setup? Something like umask settings? Or maybe a non-standard shell?

[Daan van Gent]

not that I am aware of

[Johan Commelin]

Let's do a simple check, is ~/.elan present?

[Daan van Gent]

yes

[Johan Commelin]

Ok, and ls ~/.elan/toolchains/ is empty or nonempty?

[Daan van Gent]

it contains stable/{bin,include,lib}

[Patrick Massot]

maybe source ~/.profile

[Daan van Gent]

I deleted the tutorials folder and ran "git clone https://github.com/leanprover-community/tutorials.git" instead of "leanproject get tutorials" as mentioned above, and that seemed to work. Thanks for your trouble.

[Patrick Massot]

Typing the git command by hand has nothing to do with this fix, you probably changed something else. But let's be happy that it now works

[Luuk Stehouwer]

I also got this same error, but now it seems to work.

[Johan Commelin]

If you have any idea how to improve the instructions, please let us know!

[Patrick Massot]

It seems surprisingly hard to explain those things. As you can see from the videos, we use virtual machines with a totally fresh OS, follow the instructions on the website and it just works. But we still have a constant flow of people which say it doesn't work. Any help to solve this mystery is welcome.

[Scott Morrison]

I think the github crash has made things hard today.

[Scott Morrison]

One thing to note is that the one-line install scripts are all idempotent, or close to it.

[Patrick Massot]

By the way, maybe we should periodically repost the link to the installation videos: https://www.youtube.com/playlist?list=PLlF-CfQhukNnxF1S22cNGKyfOrd380NUv

[Scott Morrison]

So you can run them a second time safely, and hopefully fix any transient issues.

[Luuk Stehouwer]

One remark: VSC gave me leanpkg.path does not exist. I googled something and then entered leanpkg configure. Now it seems to work.

[Patrick Massot]

You shouldn't do random things like this, because it makes it much harder to help you afterwards.

[Luuk Stehouwer]

OK

[Patrick Massot]

How did you end up in this state?

[Patrick Massot]

What were you trying to open and how?

[Luuk Stehouwer]

Shall I redo my installation and see if we can reproduce errors?

[Luuk Stehouwer]

I was opening the exercises in the tutorials in VSC and that is what VSC told me.

[Patrick Massot]

No, you'll probably won't be sure to have erased everything anyway

[Luuk Stehouwer]

ok lol

[Daan van Gent]

I have the same problem as Luuk: running "code tutorials/" gives an error https://pasteboard.co/Jhr9cDI.png. should I just press the button?

[Daan van Gent]

I suspect this is just the same error "leanproject get tutorials" throws after running the underlying git clone command, which I evaded by running clone in isolation

[Scott Morrison]

This is pretty benign --- I'd just press the button. :-)

[Patrick Massot]

How did you get the tutorials? This is the right question.

[Patrick Massot]

Did you use leanproject get tutorials or something else?

[Scott Morrison]

If you just used git clone, then no one has run leanpkg configure for you.

[Patrick Massot]

If you used anything else then hell is expected.

[Scott Morrison]

If you used leanproject get then hopefully it successfully did it already.

[Patrick Massot]

Scott Morrison said:

If you used leanproject get then hopefully it successfully did it already.

Unless you did that when GitHub was misbehaving earlier today and something went wrong

[Patrick Massot]

If you didn't use leanproject get but used git clone then I'd be very curious to know where you got that idea, because it may mean we left bad instructions somewhere.

[Daan van Gent]

Scott Morrison said:

git clone https://github.com/leanprover-community/tutorials.git

^

[Luuk Stehouwer]

Same story for me

[Patrick Massot]

Scott...

[Scott Morrison]

Sorry --- we were trying to get people moving during the github crash. :-)

[Scott Morrison]

But yes, my fault.

[Daan van Gent]

anyway, "leanpkg configure" gives
The terminal process failed to launch: Path to shell executable "leanpkg" does not exist.
So I guess lean is not properly installed.

[Scott Morrison]

Yes, you definitely need to reinstall.

[Daan van Gent]

what do you suggest I change this time?

[Daan van Gent]

maybe it is just a path issue? where is leanpkg supposed to be located?

[Scott Morrison]

Don't touch the path yourself!

[Scott Morrison]

:-)

[Johan Commelin]

Daan van Gent said:

maybe it is just a path issue? where is leanpkg supposed to be located?

Also in .elan.

[Scott Morrison]

Sorry. We know from experience that this causes lots of problems. Half of our install help has a root cause of someone tweaking their path themselves.

[Scott Morrison]

What OS are you on?

[Scott Morrison]

If it is a linux or macos, I would just run the one-line install script again.

[Scott Morrison]

It should be faster the second time. It should be idempotent. And it should fix any problems. :-)

[Scott Morrison]

Only once that has failed will we actually look to see what's wrong! We can just hope that something broke because of the github issues earlier today.

[Daan van Gent]

the oneliner is also idempotent in the sense that it changes nothing in the outcome

[Patrick Massot]

Well, what is really bad is to fiddle with the Lean environment variables or VSCode path settings. The shell path settings should be ok

[Scott Morrison]

Ok.

[Scott Morrison]

@Daan van Gent, could you paste the results of echo $PATH, which elan, which leanproject and which lean?

[Patrick Massot]

Daan, maybe you can come to Zoom and share your screen to help. We can even create a breakout room for this if you don't want to do it publicly.

[Scott Morrison]

That works too!

[Daan van Gent]

"echo $PATH":
"/home/daan/Documents/C++/Jury/BAPCtools/bin:/opt/devkitpro/tools/bin:/home/daan/SageMath:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games:/snap/bin:/home/daan/.local/bin"
"which elan":
""
"which leanproject":
"/home/daan/.local/bin/leanproject"
"which lean":
""

[Daan van Gent]

I take it the empty lines are bad?

[Johan Commelin]

(You can use #backticks for formatting code)

[Daan van Gent]

I shall attempt to install Zoom

[Johan Commelin]

That's a good idea anyways, otherwise you can't see the talks :wink:

[Daan van Gent]

well, the webclient is often sufficient

[Patrick Massot]

So we can confirm something went wrong. Your PATH should include "/home/daan/.elan/bin"

[Patrick Massot]

Do things improve if you run source ~/.profile?

[Scott Morrison]

If not, could you post the contents of your .profile and .bash_profile files (omitting anything sensitive first)?

[Daan van Gent]

I have no idea what a .profile file is, it seems to have been created today. If you want me to add something to PATH it should be put in .bashrc.

[Daan van Gent]

concatenating the .profile and .bashrc and sourcing .bashrc seems to fix being able to find elan at least

[Patrick Massot]

.bashrc is good enough only if you use bash...

[Daan van Gent]

the only thing in .profile in a single PATH modification anyway

[Patrick Massot]

But .profile is used globally only when you log in, that's why we recommend sourcing it by hand if you just installed and switched to another terminal

[Daan van Gent]

So code tutorials/ gives the same error popup as before, but after I press the button it now seems to do whatever it wanted to instead of produce a new error. What is the best way to see if everything is working as intended?

[Patrick Massot]

Did you actually run leanproject get tutorials?

[Scott Morrison]

If you can create a test.lean file, and write #eval 2+2 and see 4, then Lean is working.

[Patrick Massot]

Say after deleting whatever tutorials folder you could have?

[Scott Morrison]

Alternatively, you can find a begin ... end block somewhere in one of the tutorials files, and see if clicking inside that shows output in the "Lean infoview" on the right side of VS Code.

[Daan van Gent]

I deleted tutorials and ran the leanproject command. It proceeds without errors this time

[Patrick Massot]

what about code tutorials?

[Daan van Gent]

that also gives no errors,

[Patrick Massot]

Assuming you also followed the instruction about cp -r tutorials/src/exercises tutorials/src/my_exercises can you now use the VSCode file explorer to open src/my_exercises/01_equality_rewriting.lean without seeing any error message?

[John Cremona]

Do we have a checklist of things which should work by the end of the morning? I can do "code tutorials" and get a vscode window up which looks ok, but I have not tried doing anything with it yet.

[Patrick Massot]

Yes, good point John. My message right before yours is an answer.

[John Cremona]

I navigated to src/exercises/00_first_proofs_lean and in the right pane I see error messages "file 'data/real/basic' not found in the LEAN_PATH" and another similar

[Scott Morrison]

@John Cremona, how did you obtain a copy of the tutorials folder?

[Scott Morrison]

Did you use leanproject get tutorials?

[John Cremona]

You will hate this answer but I cannot remember since I did it last week.

[Scott Morrison]

No problem.

[John Cremona]

Yes I think I did do leanpackage get tutorials.

[John Cremona]

Shall I delete that directory entirely and do it again?

[Scott Morrison]

Let's try that. :-)

[Patrick Massot]

If you successfully got to the point where you can see:
image.png
then you are good to go.

[John Cremona]

After getting a fresh copy of tutorials and again navigating to the 00_first_proofs file I see no errors but only "loading..." and my laptop's fan is working hard.

[Johan Commelin]

Hmmm...

[John Cremona]

The 01 file gives error messages about "invalid import: tactic.alias"

[Johan Commelin]

Does ls _target/deps/mathlib/src/data/*.olean show anything?

[John Cremona]

(Why does vscode not allow cutting and pasting! Very annoying!)

[Johan Commelin]

It should allow that! Works for me...

[John Cremona]

Yes, lots of olean files in there

[Daan van Gent]

I managed to get a goal accomplished on "0001" of "01_equality_rewriting.lean"

[Scott Morrison]

Sounds good!

[Rob Lewis]

@John Cremona try restarting VSCode (or just the Lean server, directions in one sec)

[Scott Morrison]

@John Cremona, if that fails, you might run leanproject check in the tutorials directory and tell us what it says.

[Rob Lewis]

To restart the Lean server: ctrl-shift-p, start typing restart, click on "Lean: restart"

[Daan van Gent]

thanks for all your support! for posterity: make sure ~/.profile is sourced after installing lean via the onliner and before running leanproject get tutorials, and just press the error button if you get it when starting code tutorials.

[John Cremona]

I did the restart. Now I see no error messages just "Loading..."

[Rob Lewis]

Scott Morrison said:

John Cremona, if that fails, you might run leanproject check in the tutorials directory and tell us what it says.

@John Cremona did you try this?

[Rob Lewis]

You can also try leanproject get-mathlib-cache

[Rob Lewis]

And restart the Lean server afterward.

[John Cremona]

leanproject check says everything is fine.

[Rob Lewis]

Rob Lewis said:

You can also try leanproject get-mathlib-cache

If this doesn't work, would you like to join us in the Zoom call and share your screen? That might make debugging easier.

[John Cremona]

I did the mathlib-cahche thing and restarted but there is no change. Just "loading..."

[John Cremona]

OK I'll do join zoom...

[Rob Lewis]

Great. This is puzzling.

[John Cremona]

Can someone repost the zoom link as it is impossible to find anything on zulip with 0000's of messages

[Rob Lewis]

Join Zoom Meeting
https://vu-live.zoom.us/j/95402085900

Meeting ID: 954 0208 5900
Password: 333537

[John Cremona]

Sorry just saw the zoom thread...

[Rob Lewis]

Note that you can filter to individual streams and topics using the menus on the left.

[Rob Lewis]

#eval lean.version

[Rob Lewis]

elan --version

[Asilata Bapat]

What is the best mode to work with lean in emacs? At the moment I have installed https://github.com/leanprover/lean-mode .

[Scott Morrison]

VS Code? :-)

[Scott Morrison]

But yes, I think there's only one option for emacs, so that should be it.

[Asilata Bapat]

Thanks!

[Anne Baanen]

If you want to use spacemacs, I have a very hacked together Lean layer: https://github.com/Vierkantor/spacemacs-lean

[Asilata Bapat]

Looks great, thanks! I don't use spacemacs but I'll look through your code to get some ideas.

[Damián Gvirtz]

I followed the generic Linux instructions but somehow a file was missing: The leanpkg binary was not in ~/.elan/toolchains/leanprover-community-lean-3.17.1/bin/ . There was a leanpkg binary in ~/.elan/toolchains/stable/bin/ which I copied and at least the error message saying leanpkg is missing disappeared. Did I do anything wrong?

[Johan Commelin]

Hmm.. you shouldn't be copying those files

[Patrick Massot]

Yes, please please don't do such things.

[Johan Commelin]

At which point did you get stuck?

[Patrick Massot]

When doing that you can clearly see you're not following the instructions, so it's much better to ask before potentially messing up everything.

[Scott Morrison]

In fact, my advice on finding anything badly wrong in my .elan directory would be to delete that directory entirely, and start the installation instructions from the top!

[Scott Morrison]

And if you're just getting started, to ask here before being certain that something was badly wrong. :-)

[Patrick Massot]

To be honest those generic Linux installation instructions are obviously very much less tested than any other setup.

[Damián Gvirtz]

Thanks. I have started from top several times but every time, VSCode complained that leanpkg is missing from ~/.elan/toolchains/leanprover-community-lean-3.17.1/bin/.

[Alex J. Best]

Was there a directory ~/.elan/toolchains/leanprover-community-lean-3.17.1/ created at that point?

[Patrick Massot]

We'll start the workshop in five minutes so we'll probably leave those installation issues for a while. This afternoon you can do everything from your web browser anyway, and then we'll come back here.

[Damián Gvirtz]

Hi Alex, yes, the directory existed including folders bin, include and lib. It's just leanpkg that wasn't in bin, lean and leanchecker binaries were in bin.

[Damián Gvirtz]

I am on Arch Linux btw. No problem, I appreciate your help. Right now, a simple #eval 1+1 is working and I can also see orange bars in the tutorials project (however I am not sure whether I should see goals in the info box).

[Patrick Massot]

Seeing orange bars for a long time means something went wrong.

[Scott Morrison]

Arch linux doesn't get tested much... we may have to do some screen sharing with you to try and diagnose the problem.

[Scott Morrison]

(The orange bars mean that compiled olean files have not been successfully downloaded, and your copy of Lean is working, but working much too hard!)

[Reid Barton]

@Damián Gvirtz Do you have a directory
~/.elan/toolchains/leanprover-community-lean-3.17.1/lib/lean/leanpkg/leanpkg
containing a bunch of .lean (and maybe .olean) files?

[Damián Gvirtz]

Yes, I do have these files (and modification date is 8th July, so I assume they were downloaded, not locally generated - there used to be an "excessive memory" error when I opened the tutorials project in Lean O but it has now disappeared). To clarify, what I meant were orange bars that quickly disappear. This was given as an indication in the youtube video that it's running fine. I have also successfully reproduced the infinitude_of_primes. So I guess it is working now? It's just strange that the leanpkg script was missing from bin and I had to manually copy it.

[Dima Pasechnik]

OK, I forgot cd tutorials

[Dima Pasechnik]

my install is OK now

[Reid Barton]

@Damián Gvirtz Very strange! But leanpkg itself is a shell script that has not changed since 3.4.2, so it sounds like you should now have a fully working installation.

[Damián Gvirtz]

OK, thank you for your help and reassurance. In the interest of everyone's time I suggest, we leave it here and assume my installation is working for now. Of course, if you are worried that it is a bug with elan for generic Linux that downloads leanpkg into ~/.elan/toolchains/stable/bin but not into ~/.elan/toolchains/leanprover-community-lean-3.17.1/bin, feel free to do some digging and update me.

[Dima Pasechnik]

Dima Pasechnik said:

my install is OK now

What happened is that I decided to update tutorials installation, and absent-mindedly did git pull (as for me using straight git is a normal thing to do :/ ). This broke things. Then I tried a full reinstall, but it didn't quite work. Probably I didn't mop up enough, as I kept getting suggestions try using --force, as something exists.

[Dima Pasechnik]

Damián Gvirtz said:

OK, thank you for your help and reassurance. In the interest of everyone's time I suggest, we leave it here and assume my installation is working for now. Of course, if you are worried that it is a bug with elan for generic Linux that downloads leanpkg into ~/.elan/toolchains/stable/bin but not into ~/.elan/toolchains/leanprover-community-lean-3.17.1/bin, feel free to do some digging and update me.

Generic Linux might not even have vscode available, e.g. Gentoo Linux does not officially support vscode.

[Johan Commelin]

@Dima Pasechnik Unfortunate. Doing a git pull shouldn't blow things up. I use it quite often when working on mathlib. Presumably, if you do leanproject up afterwards, it will fix things along the way...

[Scott Morrison]

Yes. git pull is definitely allowed --- it's just that you won't automatically get any pre-compiled oleans that might be available for the commit you're moving to.

[Patrick Massot]

Just a quick reminder for everyone: today we'll assume that you managed to install Lean and its supporting tools. A good way to make sure you did it is to watch again https://www.youtube.com/watch?v=CM0wYOrYII8&list=PLlF-CfQhukNnxF1S22cNGKyfOrd380NUv&index=5 and check you can do the same on your machine.

[Patrick Massot]

So now is a good time to ask for help if it doesn't work (today's first talk will start in one hour).