Zulip Chat Archive

Stream: new members

Topic: How to install Lean

Daryl Zuniga (Nov 20 2018 at 03:43):

I downloaded the darwin zip for my Mac. Inside are bin/, include/, and lib/ folders. No readme, no install script. I can't find any installation instructions on the website. Where should I put these?
Thanks!

Chris Hughes (Nov 20 2018 at 03:49):

https://www.youtube.com/watch?v=k8U6YOK7c0M

Sayantan Majumdar (Mar 20 2019 at 07:38):

i tried the automatic installation using vscode it did not work, it kept asking me to restart lean server. then i installed elan from the gitbash and then I tried installing lean. it kept giving an error and asked me to use elan toolchain install nightly

Sayantan Majumdar (Mar 20 2019 at 07:39):

not sure what is the problem
having some problem finding the documentation too

the docs start with "Assuming you have installed Lean"

Johan Commelin (Mar 20 2019 at 07:43):

Did you find these docs https://github.com/leanprover-community/mathlib/blob/master/docs/elan.md, @Sayantan Majumdar

Johan Commelin (Mar 20 2019 at 07:43):

I don't have experience with Windows, but there is an installation video linked on that page.

Johan Commelin (Mar 20 2019 at 07:43):

I hope that helps.

Sayantan Majumdar (Mar 20 2019 at 07:44):

yeah saw the page did the elan installation too

Johan Commelin (Mar 20 2019 at 07:44):

Are the instructions in that video broken?

Sayantan Majumdar (Mar 20 2019 at 07:45):

well not sure, i didnot have to some steps they were already done

Sayantan Majumdar (Mar 20 2019 at 07:45):

like adding elan to path

Johan Commelin (Mar 20 2019 at 07:46):

Do you have a terminal?

Johan Commelin (Mar 20 2019 at 07:46):

Does which elan say anything? (I'm ot sure if which exists on Windows...)

Johan Commelin (Mar 20 2019 at 07:47):

Otherwise I'm not the best person to help you... maybe someone with a Windows box will chime in.

Sayantan Majumdar (Mar 20 2019 at 07:47):

yes
where elan

Sayantan Majumdar (Mar 20 2019 at 07:48):

i just want to know what the elan toolbox install nightly means

Sayantan Majumdar (Mar 20 2019 at 07:49):

i assume nightly build install of lean

Johan Commelin (Mar 20 2019 at 07:49):

Exactly

Johan Commelin (Mar 20 2019 at 07:49):

elan helps you to download different versions of Lean transparently.

Sayantan Majumdar (Mar 20 2019 at 07:49):

why is it asking me to install it over andover

Johan Commelin (Mar 20 2019 at 07:49):

Nowadays there aren't many releases, but there just to multiple releases a week

Sayantan Majumdar (Mar 20 2019 at 07:50):

it says no default toolchain configured

Johan Commelin (Mar 20 2019 at 07:50):

Ok, so was the automatic installation as explained in the video the first thing you tried?

Sayantan Majumdar (Mar 20 2019 at 07:50):

yeah

Sayantan Majumdar (Mar 20 2019 at 07:50):

it keeps aking me to restart lean server

Sayantan Majumdar (Mar 20 2019 at 07:50):

in VSCode

Sayantan Majumdar (Mar 20 2019 at 07:51):

now it says no default toolchain configured

Sayantan Majumdar (Mar 20 2019 at 07:51):

run elan toolchain install nightly

Johan Commelin (Mar 20 2019 at 07:52):

If that was the first thing you tried, then it means that the instructions in the video are broken. That is good to know. I'm flagging @Scott Morrison and @Bryan Gin-ge Chen who seem to know most about the installation procedures.

Sayantan Majumdar (Mar 20 2019 at 07:53):

wow wait

Johan Commelin (Mar 20 2019 at 07:53):

@Sayantan Majumdar So after that you tried the manual approach. Did you follow https://github.com/leanprover-community/mathlib/blob/master/docs/elan.md#installing-and-configuring-an-editor?

Johan Commelin (Mar 20 2019 at 07:53):

/me waits :grinning:

Sayantan Majumdar (Mar 20 2019 at 07:53):

i have to be sure its not my mistake first

Sayantan Majumdar (Mar 20 2019 at 07:54):

no

Sayantan Majumdar (Mar 20 2019 at 07:54):

i installed the extension

Sayantan Majumdar (Mar 20 2019 at 07:54):

the errors were comming there

Sayantan Majumdar (Mar 20 2019 at 07:54):

give me a sec to redo the step to be sure

Sayantan Majumdar (Mar 20 2019 at 07:57):

yeah something is wrong

Sayantan Majumdar (Mar 20 2019 at 07:58):

after you install the VSCode extension

Sayantan Majumdar (Mar 20 2019 at 07:58):

you select the gitbash as your terminal

Sayantan Majumdar (Mar 20 2019 at 07:58):

then make the file

Sayantan Majumdar (Mar 20 2019 at 07:58):

it says you need to restart a lean server

Johan Commelin (Mar 20 2019 at 08:04):

Hmmm... I don't know how to help here. I'm sorry

Johan Commelin (Mar 20 2019 at 08:04):

I hope someone else will show up with a fix.

Sayantan Majumdar (Mar 20 2019 at 08:08):

yeah thanks

Sayantan Majumdar (Mar 20 2019 at 08:08):

will figure it out eventually

Sayantan Majumdar (Mar 20 2019 at 08:08):

otherwise there's Coq

Johan Commelin (Mar 20 2019 at 08:13):

otherwise there's Coq

No, no... that's not a serious option. [/joking]

Mario Carneiro (Mar 20 2019 at 08:16):

You can always try the command line installation option

Sayantan Majumdar (Mar 20 2019 at 08:16):

tryed that

Mario Carneiro (Mar 20 2019 at 08:16):

and?

Sayantan Majumdar (Mar 20 2019 at 08:17):

I think i found a problem I have a space in my username

Sayantan Majumdar (Mar 20 2019 at 08:17):

thats the error we were discussing

Sayantan Majumdar (Mar 20 2019 at 08:17):

i was following this https://github.com/leanprover-community/mathlib/blob/master/docs/elan.md

Mario Carneiro (Mar 20 2019 at 08:17):

you can put lean into another folder without spaces

Sayantan Majumdar (Mar 20 2019 at 08:17):

i think this is cmd enough

Mario Carneiro (Mar 20 2019 at 08:18):

also I think the spaces bug is fixed, not sure

Scott Morrison (Mar 20 2019 at 08:34):

It is a bit hard to work out what you've done, and what you've tried, but the fact that you were talking about setting a path (I couldn't tell if you said you _did_ or _did not_ set one, however) suggests maybe you were doing something too complicated. You should set any paths, and just let elan configure everything.

Scott Morrison (Mar 20 2019 at 08:36):

In any case, I can confirm the VSCode only installation route on OSX is not working again. :-(

Patrick Massot (Mar 20 2019 at 08:49):

This is really a nightmare. I guess we need fresh virtual machines trying this installation procedure every night...

Patrick Massot (Mar 20 2019 at 08:52):

However it seems all my students managed to install Lean following the instructions at https://www.math.u-psud.fr/~pmassot/misc/install_lean.html. It's in French but it basically says: install Git bash, accepting all default options, type the magic elan line curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh, accepting all default options, restart Windows session, install VScode, accepting all default options, install the Lean extension. But maybe I was lucky and no student have space in username

Johan Commelin (Mar 20 2019 at 09:09):

@Sayantan Majumdar Congratulations!

Scott Morrison (Mar 21 2019 at 05:30):

Ok, I've I think fixed the "offer to install Elan" feature in VS Code. I think it just hasn't been working at all since my previous "fix", sadly. There's a PR waiting, and it would be great if someone could test it, either before or after Gabriel merges it.

Bryan Gin-ge Chen (Mar 21 2019 at 06:44):

Thanks for following up on this, I've just tested the installation procedure via the extension on macOS and windows and it works! Hooray!

Scott Morrison (Mar 21 2019 at 07:10):

Thanks for testing!

Simon Hudon (Mar 21 2019 at 14:12):

Btw what is the status of installation on three major platforms for newcomers? Is there a straightforward happy path?

Kevin Buzzard (Mar 21 2019 at 14:35):

@Daryl Zuniga @Sayantan Majumdar you were both having trouble at the start of this thread. The devs have tried to fix the problem. Have you both got things working now?

Bryan Gin-ge Chen (Mar 21 2019 at 16:32):

After @Scott Morrison 's PR is merged, installing lean via elan via the VS code extension should work (at least it worked for me on both macOS and Windows).

Last updated: Dec 20 2023 at 11:08 UTC