Zulip Chat Archive

Stream: new members

Topic: Installation questions


view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 00:34):

Here's a new thread for installation questions.

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 00:34):

@Charles Rezk What system are you using, e.g. windows, mac, linux? There's some basic advice by Kevin Buzzard here.

view this post on Zulip Charles Rezk (Oct 06 2018 at 00:35):

Linux. Yes I'm trying to follow the instructions on that page.

view this post on Zulip Charles Rezk (Oct 06 2018 at 00:35):

I've compiled lean.

view this post on Zulip Charles Rezk (Oct 06 2018 at 00:35):

I've added the mathlib package.

view this post on Zulip Charles Rezk (Oct 06 2018 at 00:35):

I've installed the vscode thing.

view this post on Zulip Charles Rezk (Oct 06 2018 at 00:35):

I've started it up, and tried to run an example.

view this post on Zulip Charles Rezk (Oct 06 2018 at 00:36):

For some reason it strangely does not find the lean executable.

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 00:37):

Are you able to run lean from the terminal?

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 00:37):

I guess so, if you were able to add mathlib with leanpkg.

view this post on Zulip Charles Rezk (Oct 06 2018 at 00:37):

I can do "lean --version"

view this post on Zulip Charles Rezk (Oct 06 2018 at 00:37):

When vscode tries to run the lean executable, it for some reason puts in an extra comma

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 00:39):

I guess you're seeing an error message somewhere. What does it say exactly?

view this post on Zulip Charles Rezk (Oct 06 2018 at 00:40):

Lean: Error: Command failed: /home/rezk/git/lean/bin/lean, --version
/bin/sh: /home/rezk/git/lean/bin/lean,: No such file or directory

view this post on Zulip Charles Rezk (Oct 06 2018 at 00:41):

I don't know why there is an extra comma in there, but that is presumably why it is failing

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 00:42):

Could you check your VS code settings? Under "Extensions > Lean configuration" there should be a box that says "Executable path"

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 00:42):

If there's not an extra comma in there then I'm stumped.

view this post on Zulip Charles Rezk (Oct 06 2018 at 00:43):

How do I find this box?

view this post on Zulip Charles Rezk (Oct 06 2018 at 00:43):

I have been trying to set the executable path in "User Settings", according to the instructions, but that seems to have literally no effect.

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 00:44):

Did you edit your settings.json file to add the "lean.executablePath" option as in Kevin's instructions? Maybe there's a misplaced quote there.

view this post on Zulip Charles Rezk (Oct 06 2018 at 00:46):

Yes I have tried that, assuming I am doing it correctly. As far as I can tell, it complety ignores what I put there. I can give a giberish path, and I still get the exact same error message I gave you above.

view this post on Zulip Kevin Buzzard (Oct 06 2018 at 00:46):

Ctrl + comma might take you to preferences

view this post on Zulip Charles Rezk (Oct 06 2018 at 00:46):

Some how it is getting an incorrect path from somewhere else

view this post on Zulip Kevin Buzzard (Oct 06 2018 at 00:47):

Or something like file -> settings -> preferences

view this post on Zulip Scott Morrison (Oct 06 2018 at 00:47):

Do you want to copy-paste your "settings.json" file here?

view this post on Zulip Scott Morrison (Oct 06 2018 at 00:50):

@Charles Rezk, did you at any point set the environment variable LEAN_PATH?

view this post on Zulip Charles Rezk (Oct 06 2018 at 00:51):

No, there is no $LEAN_PATH

view this post on Zulip Scott Morrison (Oct 06 2018 at 00:51):

Could you show your settings.json file?

view this post on Zulip Charles Rezk (Oct 06 2018 at 00:51):

From what it says in USer Settings, the settings.json file is:

view this post on Zulip Charles Rezk (Oct 06 2018 at 00:52):

{ "lean.executablePath": "/home/rezk/git/lean/bin/lean"
}

view this post on Zulip Charles Rezk (Oct 06 2018 at 00:52):

I don't know where this file is actually kept

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 00:53):

On linux it's apparently $HOME/.config/Code/User/settings.json

view this post on Zulip Scott Morrison (Oct 06 2018 at 00:53):

Here's another suggestion:

view this post on Zulip Scott Morrison (Oct 06 2018 at 00:53):

the best way to install Lean is actually to use elan

view this post on Zulip Scott Morrison (Oct 06 2018 at 00:53):

from <https://github.com/Kha/elan>

view this post on Zulip Charles Rezk (Oct 06 2018 at 00:54):

I've been doing this for several hours. I'm not starting again.

view this post on Zulip Scott Morrison (Oct 06 2018 at 00:54):

e.g. just by running curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh in a terminal

view this post on Zulip Scott Morrison (Oct 06 2018 at 00:54):

Ok :-)

view this post on Zulip Scott Morrison (Oct 06 2018 at 00:54):

(My experience is that installing Lean via elan takes less than a minute. :-)

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 00:54):

In particular, you won't have to rebuild lean from source that way.

view this post on Zulip Charles Rezk (Oct 06 2018 at 00:55):

OK, that explains it. The actually "settings.json" file is different than what vscode is showing me

view this post on Zulip Scott Morrison (Oct 06 2018 at 00:55):

(The advantage is that you don't have to compile anything, you don't have to set any paths in VS Code, and elan will automatically switch between Lean versions if you have different projects requiring different versions.)

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 00:57):

The installation process will hopefully be a lot, lot easier once Scott's PR to the VS code extension is merged.

view this post on Zulip Charles Rezk (Oct 06 2018 at 00:57):

I restarted vscode, and now it shows the actually physical file in "Settings", and also I don't get that error any more when I try to "Restart: Lean"

view this post on Zulip Charles Rezk (Oct 06 2018 at 00:58):

Now nothing happens when I do that, which doesn't seem like an improvement

view this post on Zulip Scott Morrison (Oct 06 2018 at 00:59):

"Nothing happening" might be the right thing! Lean doesn't say anything upon a successful start up, until you actually enter something in a .lean file.

view this post on Zulip Scott Morrison (Oct 06 2018 at 01:00):

Can you save a file, e.g. as test.lean, and enter something in it, such as #eval 2+2?

view this post on Zulip Scott Morrison (Oct 06 2018 at 01:00):

You should then get a green squiggle under it, and hovering the mouse there should show 4.

view this post on Zulip Charles Rezk (Oct 06 2018 at 01:04):

I have tried that. Nothing happens, no green squiggle

view this post on Zulip Charles Rezk (Oct 06 2018 at 01:05):

Wait, now it is.

view this post on Zulip Charles Rezk (Oct 06 2018 at 01:05):

Maybe it works now

view this post on Zulip Mario Carneiro (Oct 06 2018 at 01:07):

If you see orange bars on the sidebar that means it's in progress and you should wait

view this post on Zulip Mario Carneiro (Oct 06 2018 at 01:07):

you can also see status information on the bottom left which will tell you if lean is dead or just busy

view this post on Zulip Charles Rezk (Oct 06 2018 at 01:08):

I think it's working now

view this post on Zulip Mario Carneiro (Oct 06 2018 at 01:08):

You should test mathlib imports if you intend to use it, e.g. import data.nat.prime

view this post on Zulip Charles Rezk (Oct 06 2018 at 01:12):

OK

view this post on Zulip Charles Rezk (Oct 06 2018 at 01:17):

I think this computer is going to be too slow for this.

view this post on Zulip Mario Carneiro (Oct 06 2018 at 01:18):

you may need to compile the lean sources if everything is running slow

view this post on Zulip Mario Carneiro (Oct 06 2018 at 01:18):

i.e. run lean --make in the library directoy

view this post on Zulip Charles Rezk (Oct 06 2018 at 01:20):

What is the library directory?

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 01:22):

The mathlib you added to your package should be in _target/deps/mathlib relative to the package root; running lean --make in that directory should make importing mathlib much faster.

view this post on Zulip Scott Morrison (Oct 06 2018 at 02:41):

Hi @Bryan Gin-ge Chen , just correcting that suggestion: in general it is safer to run lean —make _target/deps/mathlib from the main project directory, rather than changing into that subdirectory and running lean —make. If there is a version mismatch between the project and mathlib, running lean in the subdirectory will just give you olean files that won’t be usable.

view this post on Zulip Scott Morrison (Oct 06 2018 at 02:41):

(If there’s no version mismatch, there’s no problem, but we seem to have regular problems with this.)

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 02:43):

Thanks! That's good to know.

view this post on Zulip Scott Morrison (Oct 06 2018 at 02:49):

Perhaps we should add a command in VS Code “compile all dependencies in background” to help people with this.

view this post on Zulip Johan Commelin (Oct 09 2018 at 16:41):

@Charles Rezk Did you get the install working in the end?

view this post on Zulip Charles Rezk (Oct 09 2018 at 16:58):

I did. I'm not really sure how do actually do anything interesting, the mathlib files are hard for me to interpret.

view this post on Zulip Kevin Buzzard (Oct 09 2018 at 17:03):

Pick a project, get stuck, ask here, people will try to help :-) At least that's how I did it

view this post on Zulip Johan Commelin (Oct 09 2018 at 17:05):

@Charles Rezk I suggest you write a short post in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/subject/Introductions.

view this post on Zulip Johan Commelin (Oct 09 2018 at 17:05):

Tell us where you are based and what kind of stuff you like.

view this post on Zulip Johan Commelin (Oct 09 2018 at 17:05):

And like Kevin said, just hang around and ask questions.

view this post on Zulip Wojciech Nawrocki (Jan 14 2019 at 23:20):

Is it normal for compilation of mathlib master to fail miserably on nightly Lean? I made a package with leanpkg +nightly new, then added mathlib and lean --make _target/deps/mathlib/ shows errors on everything, e.g. relator.lean:13:43: error: unknown identifier 'left_unique'.

view this post on Zulip Kenny Lau (Jan 14 2019 at 23:23):

We use 3.4.1 Lean

view this post on Zulip Bryan Gin-ge Chen (Jan 14 2019 at 23:33):

see also https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mathlib.20is.20broken


Last updated: May 12 2021 at 03:23 UTC