Installation questions

Stream: new members

[Bryan Gin-ge Chen]

Here's a new thread for installation questions.

[Bryan Gin-ge Chen]

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

[Charles Rezk]

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

[Charles Rezk]

I've compiled lean.

[Charles Rezk]

I've added the mathlib package.

[Charles Rezk]

I've installed the vscode thing.

[Charles Rezk]

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

[Charles Rezk]

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

[Bryan Gin-ge Chen]

Are you able to run lean from the terminal?

[Bryan Gin-ge Chen]

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

[Charles Rezk]

I can do "lean --version"

[Charles Rezk]

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

[Bryan Gin-ge Chen]

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

[Charles Rezk]

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

[Charles Rezk]

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

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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

[Charles Rezk]

How do I find this box?

[Charles Rezk]

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

[Bryan Gin-ge Chen]

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.

[Charles Rezk]

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.

[Kevin Buzzard]

Ctrl + comma might take you to preferences

[Charles Rezk]

Some how it is getting an incorrect path from somewhere else

[Kevin Buzzard]

Or something like file -> settings -> preferences

[Scott Morrison]

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

[Scott Morrison]

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

[Charles Rezk]

No, there is no $LEAN_PATH

[Scott Morrison]

Could you show your settings.json file?

[Charles Rezk]

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

[Charles Rezk]

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

[Charles Rezk]

I don't know where this file is actually kept

[Bryan Gin-ge Chen]

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

[Scott Morrison]

Here's another suggestion:

[Scott Morrison]

the best way to install Lean is actually to use elan

[Scott Morrison]

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

[Charles Rezk]

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

[Scott Morrison]

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

[Scott Morrison]

Ok :-)

[Scott Morrison]

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

[Bryan Gin-ge Chen]

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

[Charles Rezk]

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

[Scott Morrison]

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

[Bryan Gin-ge Chen]

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

[Charles Rezk]

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"

[Charles Rezk]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Charles Rezk]

I have tried that. Nothing happens, no green squiggle

[Charles Rezk]

Wait, now it is.

[Charles Rezk]

Maybe it works now

[Mario Carneiro]

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

[Mario Carneiro]

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

[Charles Rezk]

I think it's working now

[Mario Carneiro]

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

[Charles Rezk]

OK

[Charles Rezk]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Charles Rezk]

What is the library directory?

[Bryan Gin-ge Chen]

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.

[Scott Morrison]

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.

[Scott Morrison]

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

[Bryan Gin-ge Chen]

Thanks! That's good to know.

[Scott Morrison]

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

[Johan Commelin]

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

[Charles Rezk]

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

[Kevin Buzzard]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Wojciech Nawrocki]

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

[Kenny Lau]

We use 3.4.1 Lean

[Bryan Gin-ge Chen]

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