vscode

Stream: lean4

[Andrea]

I have just freshly installed on Windows Lean4. I have created a project using the command, got myself a .proj file and a .lean file and now trying to create my first proof. It gives me an error on import:

import data.nat.prime

open nat

#eval 11

On the first line the errors is a simple blue underline with no message. This is preventing the infoview from displaying any valuable info. Please note that I have installed the Lean4 extension and that I have opened VSCode into the folder of my project containing the .proj file.

[Julian Berman]

That looks like it's going to be Lean 3 code -- data.nat.prime is a thing in mathlib (which is a Lean 3 project), as is nat -- if you're just starting out and want to use things from mathlib you'll need lean 3.

[Andrea]

Thanks @Julian Berman So you are basically telling me the whole mathlib is completely inaccessible to Lean4? So how is one supposed to use Lean4?

[Mario Carneiro]

Porting has to be done essentially from scratch. You can watch the progress at the #mathlib4 stream but I fully expect it to take at least a year

[Mario Carneiro]

If you care about using mathlib, then you should just stick with lean 3 for now

[Andrea]

Thanks @Mario Carneiro and @Julian Berman your comments were insightful and helpful.

[Kevin Buzzard]

If you are interested in doing mathematics in Lean with the maths library then you should be following the instructions at the leanprover-community website, lean4 has not even had a stable release yet

[Kevin Buzzard]

https://leanprover-community.github.io/get_started.html

[Netchaiev]

Hello, I am struggling with lean4 on vscode : now, when I open a lean file, vs-code tells me :
Lean (version 4.0.0-nightly-2021-12-12, commit a91b8619196b, Release)
which seems nice but nothing happen then ... Capture-décran-2021-12-12-à-11.13.01.png

[Kevin Buzzard]

I don't know too much about lean 4 but with lean 3 you can't just open a random lean file, you need to open a file contained in a lean project. You can make a lean 4 protect with something like leanpkg new project_name, and then you have to open the root directory of the project with VS Code

[Horatiu Cheval]

Though I don't think leanpkg new works for Lean4, leanpkg help lists only the init, configure and build commands. It's preferable to use lake new ProjectName.