Lean 4 installation issues

Stream: lean4

[Mario Carneiro]

what did you do?

[Isaia Nisoli]

I followed the instructions on the Lean4 Manual: tried once with the Basic setup, did not work, ran "elan self uninstall" and ran the Quickstart setup from the same manual but I have the same problems, both with stable and nightly.
When I call leanpkg from the command line I get an uncaught exception message and vscode gives an error message, he cannot start lean in server mode

[Mario Carneiro]

Please post the error messages and the commands you ran

[Isaia Nisoli]

isaia@aiace-laptop:~/Isabelle/Isabelle2021$ leanpkg
uncaught exception: Lean package manager, version 4.0.0

Usage: leanpkg <command>

init <name> create a Lean package in the current directory
configure download and build dependencies
build [<args>] configure and build *.olean files

See leanpkg help <command> for more information on a specific command.

[Isaia Nisoli]

In VSCode I get a Server has stopped with error code

[Isaia Nisoli]

And leanpkg.path does not exist

[Isaia Nisoli]

the OS is Ubuntu 20.10

[Mario Carneiro]

As the error message says, leanpkg requires a subcommand like leanpkg init MyProject or leanpkg build

[Mario Carneiro]

I think lean 4 doesn't use leanpkg.path anymore, that's a lean 3 thing

[Isaia Nisoli]

I will check now if there is amismatch in the VSCode extension

[Isaia Nisoli]

ok, it seems like I installed the old lean extension instead of the lean4 extension

[Mario Carneiro]

Are you using elan?

[Mario Carneiro]

https://github.com/leanprover/elan

[Isaia Nisoli]

yes, I installed everything through elan

[Isaia Nisoli]

I will try to restart vscode, it gave me an error, "The Lean 4 server crashed 5 times in the last 3 minutes. The server will not be restarted."

[Mario Carneiro]

what does lean --version at the console give?

[Mario Carneiro]

If it says lean 3, try elan override set leanprover/lean4:nightly

[Isaia Nisoli]

Lean (version 4.0.0-m2, commit 26dda3f63d88, Release)

[Mario Carneiro]

you might still want to use nightly in case there is some bug that's been fixed

[Isaia Nisoli]

VSCode is giving this output and then crashes
Watchdog error: Got unknown document URI (file:///home/isaia/lean/my_playground/gatto.lean)
[Info - 6:32:39 PM] Connection to server got closed. Server will restart.
[Error - 6:32:39 PM] Request textDocument/documentSymbol failed.
Error: Connection got disposed.
at Object.dispose (/home/isaia/.vscode/extensions/leanprover.lean4-0.0.25/out/extension.js:2:145943)
at Object.dispose (/home/isaia/.vscode/extensions/leanprover.lean4-0.0.25/out/extension.js:2:226115)
at C.handleConnectionClosed (/home/isaia/.vscode/extensions/leanprover.lean4-0.0.25/out/extension.js:2:226328)
at C.handleConnectionClosed (/home/isaia/.vscode/extensions/leanprover.lean4-0.0.25/out/extension.js:2:286716)
at t (/home/isaia/.vscode/extensions/leanprover.lean4-0.0.25/out/extension.js:2:224417)
at invoke (/home/isaia/.vscode/extensions/leanprover.lean4-0.0.25/out/extension.js:2:147556)
at o.fire (/home/isaia/.vscode/extensions/leanprover.lean4-0.0.25/out/extension.js:2:148317)
at Y (/home/isaia/.vscode/extensions/leanprover.lean4-0.0.25/out/extension.js:2:135201)
at invoke (/home/isaia/.vscode/extensions/leanprover.lean4-0.0.25/out/extension.js:2:147556)
at o.fire (/home/isaia/.vscode/extensions/leanprover.lean4-0.0.25/out/extension.js:2:148317)
at g.fireClose (/home/isaia/.vscode/extensions/leanprover.lean4-0.0.25/out/extension.js:2:156198)
at Socket.<anonymous> (/home/isaia/.vscode/extensions/leanprover.lean4-0.0.25/out/extension.js:2:157783)
at Socket.emit (events.js:327:22)
at Pipe.<anonymous> (net.js:673:12)

[Isaia Nisoli]

I will try the nightly

[Chris B]

Yeah, you need to use nightly: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/vscode-lean4.20Doesn't.20Work.20When.20I.20Switch.20Files/near/232024638

[Chris B]

For now at least.

[Isaia Nisoli]

ah, perfect! Now it seems to work! Thank you so much!

[Jürgen Uhl]

After installing Git (Windows 11), the lean4 VSCode extension and having that install elan / lean, I get the error "Watchdog error: no such file or directory (error code: 2)". Any idea, what I did wrong?

[Shreyas Srinivas]

Jürgen Uhl said:

After installing Git (Windows 11), the lean4 VSCode extension and having that install elan / lean, I get the error "Watchdog error: no such file or directory (error code: 2)". Any idea, what I did wrong?

What's your directory tree like (suitably anonymised ofc)?

[Jürgen Uhl]

which directory tree?

[Shreyas Srinivas]

where you have opened vscode

[Jürgen Uhl]

well, i open vsc from the startup icon and then select the working directory. The WD is D:\Develop\VSCode\Lean

[Jürgen Uhl]

How would I find out the startup directory?

[Shreyas Srinivas]

okay, let me start a few step earlier

[Shreyas Srinivas]

are commands like elan --version and lake version showing some output?

[Jürgen Uhl]

elan 3.0.0 (cdb40bff5 2023-09-08)

[Jürgen Uhl]

Lake version 5.0.0-a832f39 (Lean version 4.1.0)

[Shreyas Srinivas]

okay perfect. Now Please follow the steps I suggest below to create a new lean project and open it in vscode

[Shreyas Srinivas]

cd <folder where you want to create your project>

[Shreyas Srinivas]

lake new <project name>

[Shreyas Srinivas]

cd <project name>

[Shreyas Srinivas]

code .

[Jürgen Uhl]

error

[Shreyas Srinivas]

which step?
what error?

[Jürgen Uhl]

oh, should I have run that in VS Code console or windows consloe or powershell or what?

[Shreyas Srinivas]

usually use powershell (or even better for convenience, use the terminal that windows comes with these days)

[Jürgen Uhl]

I ran in vs console and the last "code ." gave an error

[Shreyas Srinivas]

vs console? Inside vscode?

[Jürgen Uhl]

yes

[Scott Morrison]

What is the error?

[Jürgen Uhl]

code : Die Benennung "code" wurde nicht als Name eines Cmdlet, einer Funktion, einer Skriptdatei oder eines ausführbaren Programms erkannt.
Überprüfen Sie die Schreibweise des Namens, oder ob der Pfad korrekt ist (sofern enthalten), und wiederholen Sie den Vorgang.
In Zeile:1 Zeichen:1

• code .
• ~~~~
  + CategoryInfo : ObjectNotFound: (code:String) [], CommandNotFoundException
  + FullyQualifiedErrorId : CommandNotFoundException

[Jürgen Uhl]

you understand that or should i translate?

[Shreyas Srinivas]

THat's because you are running the command in the cmd shell

[Jürgen Uhl]

so where should I run it?

[Shreyas Srinivas]

On windows 11 you should have an app called terminal

[Jürgen Uhl]

but that does not know "code", apparently

[Jürgen Uhl]

maybe when installing vscode i did not add the path

[Shreyas Srinivas]

wait. Once you open the terminal, windows adds extra steps

[Shreyas Srinivas]

okay that's possible.

[Shreyas Srinivas]

Please check the PATH variable first.

[Jürgen Uhl]

okay, started it with explicit path.

[Jürgen Uhl]

says "Waiting for Lean Server to start..."

[Shreyas Srinivas]

Is your toolchain on your PATH variable?

[Shreyas Srinivas]

And did it start?

[Jürgen Uhl]

Seems to work now.

[Shreyas Srinivas]

Awesome

[Jürgen Uhl]

Sorry, what is "toolchain"

[Shreyas Srinivas]

the collection of lean the compiler, lake the build tool, and some basic libraries (not Mathlib)

[Jürgen Uhl]

and where would I find that?

[Shreyas Srinivas]

cd ~/.elan

[Shreyas Srinivas]

In powershell. AFAIK, windows cmd doesn't know the command cd

[Shreyas Srinivas]

For simplicity you might want to make powershell your default terminal in your windows settings

[Jürgen Uhl]

ah, found it. And that should go into the Windows PATH, correct?

[Jürgen Uhl]

Well, anyway, seems to be working now. Thanks a lot! (Could I have found that by myself from the docs, btw.?)

[Shreyas Srinivas]

I would not recommend tinkering with a working setup. If vscode can find the lean extension and you are able to execute commands like elan --version and lake --version you should already have the correct PATH variable

[Shreyas Srinivas]

I was on autopilot when asking you about the lean toolchain being on path question

[Shreyas Srinivas]

Jürgen Uhl said:

Well, anyway, seems to be working now. Thanks a lot! (Could I have found that by myself from the docs, btw.?)

Good question. I think yes, but the docs are split between multiple places at the moment. There is an ongoing effort to rationalise and reorganise all this.

[Anotherpieceofmyhead]

Hello guys, Im new here, sorry If my issue is misplaced.
Mac M1, I cant build project with mathlib included (I even cant build the pre-existed project, I tried mathematics_in_lean as was suggested), the error is "unknown package 'Mathlib'", Is this a common issue or is this me?:)

[Scott Morrison]

It's probably you not following the instructions exactly. :-)

[Scott Morrison]

Did you open the correct folder in VSCode? (it's essential that you use "open folder", rather than opening an individual file, and you must open the folder containing the lakefile.lean).

[Scott Morrison]

@Anotherpieceofmyhead

[Anotherpieceofmyhead]

well, that makes me sad, but thats possible:)
Yes, i was opening a folder.
To be honest I thought that it might be my mistake, but after failing to build the https://leanprover-community.github.io/mathematics_in_lean/mathematics_in_lean.pdf I was wondering if this is something common

[Anotherpieceofmyhead]

Nah, I figured it out, you were right about the folders and I feel ashamed :D

Thanks a lot

[Anotherpieceofmyhead]

I was opening the broader folder all the time, and lean didnt like it

[Michael Stoll]

One of my students reports the following problem. After following the first steps of these instructions (install VSCode, install git, install the Lean4 extension, set up a text file), after clicking the Install Lean using Elan button, an error message appears (sorry for the German)

(prompt)> Start-BitsTransfer -Source
 "https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1"
 -Destination "elan-init.ps1"
 Die Benennung "Start-BitsTransfer" wurde nicht als Name eines Cmdlet,
 einer Funktion, einer Skriptdatei oder eines ausführbaren Programms
 erkannt. Überprüfen Sie die Schreibweise des Namens, oder ob der Pfad
 korrekt ist (sofern enthalten), und wiederholen Sie den Vorgang.
 Bei Zeile:1 Zeichen:19
 + Start-BitsTransfer <<<<  -Source
 "https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1"
 -Destination "elan-init.ps1"
      + CategoryInfo          : ObjectNotFound:
 (Start-BitsTransfer:String) [], CommandNotFoundException
      + FullyQualifiedErrorId : CommandNotFoundException

To my eyes, it looks like the process tries to run a command Start-BitsTransfer, which does not exist or cannot be found in the PATH. Any ideas? (I'm working with Linux myself and don't know a lot about Windows...)

[Julian Berman]

I don't know anything about Windows either, but searching seems to suggest that error means that the student is on an old Powershell (1.0). What version of Windows is this, do you know?

[Michael Stoll]

I don't know, but I've asked.

[Julian Berman]

Assuming I can interpret the page I'm reading I believe the answer will be "quite old", as I think this is saying Powershell 2.0 is present already even in Windows 7. But let's see.

[Julian Berman]

Regardless, it might be asking them to follow https://learn.microsoft.com/en-us/powershell/scripting/install/installing-powershell-on-windows?view=powershell-7.3 is going might be the next step.

[Michael Stoll]

I'm still waiting for an answer regarding the Windows version. Going to bed now...