Zulip Chat Archive

Stream: new members

Topic: How to install Lean


view this post on Zulip 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!

view this post on Zulip Chris Hughes (Nov 20 2018 at 03:49):

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

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 20 2019 at 07:43):

I hope that helps.

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 07:44):

yeah saw the page did the elan installation too

view this post on Zulip Johan Commelin (Mar 20 2019 at 07:44):

Are the instructions in that video broken?

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 07:45):

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

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 07:45):

like adding elan to path

view this post on Zulip Johan Commelin (Mar 20 2019 at 07:46):

Do you have a terminal?

view this post on Zulip Johan Commelin (Mar 20 2019 at 07:46):

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

view this post on Zulip 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.

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 07:47):

yes
where elan

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 07:48):

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

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 07:49):

i assume nightly build install of lean

view this post on Zulip Johan Commelin (Mar 20 2019 at 07:49):

Exactly

view this post on Zulip Johan Commelin (Mar 20 2019 at 07:49):

elan helps you to download different versions of Lean transparently.

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 07:49):

why is it asking me to install it over andover

view this post on Zulip Johan Commelin (Mar 20 2019 at 07:49):

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

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 07:50):

it says no default toolchain configured

view this post on Zulip Johan Commelin (Mar 20 2019 at 07:50):

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

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 07:50):

yeah

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 07:50):

it keeps aking me to restart lean server

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 07:50):

in VSCode

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 07:51):

now it says no default toolchain configured

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 07:51):

run elan toolchain install nightly

view this post on Zulip 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.

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 07:53):

wow wait

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Mar 20 2019 at 07:53):

/me waits :grinning:

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 07:53):

i have to be sure its not my mistake first

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 07:54):

no

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 07:54):

i installed the extension

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 07:54):

the errors were comming there

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 07:54):

give me a sec to redo the step to be sure

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 07:57):

yeah something is wrong

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 07:58):

after you install the VSCode extension

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 07:58):

you select the gitbash as your terminal

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 07:58):

then make the file

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 07:58):

it says you need to restart a lean server

view this post on Zulip Johan Commelin (Mar 20 2019 at 08:04):

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

view this post on Zulip Johan Commelin (Mar 20 2019 at 08:04):

I hope someone else will show up with a fix.

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 08:08):

yeah thanks

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 08:08):

will figure it out eventually

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 08:08):

otherwise there's Coq

view this post on Zulip Johan Commelin (Mar 20 2019 at 08:13):

otherwise there's Coq

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

view this post on Zulip Mario Carneiro (Mar 20 2019 at 08:16):

You can always try the command line installation option

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 08:16):

tryed that

view this post on Zulip Mario Carneiro (Mar 20 2019 at 08:16):

and?

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 08:17):

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

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 08:17):

thats the error we were discussing

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 08:17):

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

view this post on Zulip Mario Carneiro (Mar 20 2019 at 08:17):

you can put lean into another folder without spaces

view this post on Zulip Sayantan Majumdar (Mar 20 2019 at 08:17):

i think this is cmd enough

view this post on Zulip Mario Carneiro (Mar 20 2019 at 08:18):

also I think the spaces bug is fixed, not sure

view this post on Zulip 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.

view this post on Zulip 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. :-(

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 20 2019 at 09:09):

@Sayantan Majumdar Congratulations!

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Scott Morrison (Mar 21 2019 at 07:10):

Thanks for testing!

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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: May 11 2021 at 12:15 UTC