language servers?

Stream: new members

[crab]

why the red on the infoview? image.png

[Eric Rodriguez]

just press try again, the server can shut down sometimes

[Eric Rodriguez]

or try the > Lean: restart server command

[crab]

Eric Rodriguez said:

or try the > Lean: restart server command

I will try

[crab]

It works now. How can I run the code?

[Arthur Paulino]

crab said:

It works now. How can I run the code?

You can run it with $ lean --run hi.lean

Or, if you're inside a lake project, you can build before running with lake build. This will generate a binary file that you can run in your terminal

[Arthur Paulino]

But I suspect you didn't start a lake project

[crab]

Thank you!

[crab]

Its not recognizing the command lean

[crab]

I thought I added it to PATH

[Arthur Paulino]

Hm, this is not the best way to setup your Lean environment. Funnily, I made this very same mistake :rofl:
The right lean binary is supposed to be found by elan, depending on the configuration of the Lean project you're in.
Can you do $ lake new MyProj?

[Arthur Paulino]

I had added lean to my path manually too. But then I removed it

[crab]

Arthur Paulino said:

Hm, this is not the best way to setup your Lean environment. Funnily, I made this very same mistake :rofl:
The right lean binary is supposed to be found by elan, depending on the configuration of the Lean project you're in.
Can you do $ lake new MyProj?

What is elan?

[crab]

image.png

[Arthur Paulino]

I will show you how a properly set Lean environment is supposed to work.
I have this project called LeanMusic. It uses a certain version of Lean:

/LeanMusic$ lean --version
Lean (version 4.0.0-nightly-2021-12-28, commit 748c9ab73a47, Release)

But if I run the same command inside another Lean project, it might say something else:

/LeanMySQL$ lean --version
Lean (version 4.0.0-nightly-2021-12-02, commit c54caa1a1fdf, Release)

[Arthur Paulino]

You can find more info about lake here

[crab]

Thank you

[Arthur Paulino]

This link should help you setting up Lean on Windows:
https://leanprover-community.github.io/install/windows.html

[crab]

That is what I was looking for! Thank you!

[crab]

already problems...

$ curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
info: downloading installer
Archive:  elan-init.zip
  inflating: elan-init.exe

Welcome to Lean!

This will download and install Elan, a tool for managing different Lean
versions used in packages you create or download. It will also install a
default version of Lean and its package manager, leanpkg, for editing files not
belonging to any package.

It will add the leanpkg, lean, and elan commands to Elan's bin directory,
located at:

  C:\Users\Joseph\.elan\bin

This path will then be added to your PATH environment variable by modifying the
HKEY_CURRENT_USER/Environment/PATH registry key.

You can uninstall at any time with elan self uninstall and these changes will
be reverted.

Current installation options:

     default toolchain: stable
  modify PATH variable: yes

1) Proceed with installation (default)
2) Customize installation
3) Cancel installation
1

error: could not create link from 'C:\Users\Joseph\.elan\bin\elan.exe' to 'C:\Users\Joseph\.elan\bin\lake.exe'

[crab]

What is wrong?

[Arthur Paulino]

I think another Windows user can help you better on this one (I'm a Linux user)

[crab]

Ok. Well thank you for your help.

[Mario Carneiro]

try running it as administrator?

[crab]

Mario Carneiro said:

try running it as administrator?

Ah, good idea!

[crab]

No, same thing.

[Mario Carneiro]

is there anything funny located at C:\Users\Joseph\.elan\bin\elan.exe or C:\Users\Joseph\.elan\bin\lake.exe?

[Mario Carneiro]

you could try deleting the .elan directory and trying again

[crab]

ok

[crab]

i deleted it

[Arthur Paulino]

Remember to undo the manual addition of lean to the path

[Arthur Paulino]

I think this link can be misleading :/
https://leanprover.github.io/download/

I mean, yeah, the binaries are there, but in practice you're not supposed to get them from there...

[crab]

image.png

[crab]

Lean is still not recognized

[Arthur Paulino]

Now you need to be inside a Lean project. Try $ lake new MyProj

[Arthur Paulino]

If it works, place the hi.lean file there and, from within the MyProj directory, call lean --run hi.lean

[crab]

image.png

[crab]

something didnt work correctly

[Arthur Paulino]

Try closing and opening the terminal again

[Alex J. Best]

If you are trying to install lean 3 which is what the tutorials I linked to yesterday refer to, you do not want/need lake. If you follow these instructions https://leanprover-community.github.io/install/windows.html where do you get stuck?

[crab]

Alex J. Best said:

If you are trying to install lean 3 which is what the tutorials I linked to yesterday refer to, you do not want/need lake. If you follow these instructions https://leanprover-community.github.io/install/windows.html where do you get stuck?

I did the whole process

[crab]

Arthur Paulino said:

Try closing and opening the terminal again

ok

[crab]

now i get

[crab]

image.png image.png

[Mauricio Collares]

This is good, actually! Lake is not yet in a stable Lean4 release, so this is why you get the error. Try running elan default leanprover/lean4:nightly first.

[Mauricio Collares]

But, like Alex said, if you are interested in Lean 3 (for example, if you want to prove theorems using mathlib) you don't want lake.

[Mauricio Collares]

You can use both lean3 and lean4 for different purposes, and elan will take care of everything. As long as you know that lean3 uses leanproject (a frontend to leanpkg that you may need to install separately) and lean4 uses lake, you should be good.

[crab]

i see

[crab]

So what should I do to create a lake project?

[Arthur Paulino]

did elan default leanprover/lean4:nightly work?

[crab]

Arthur Paulino said:

did elan default leanprover/lean4:nightly work?

I assume so

[crab]

image.png

[Arthur Paulino]

now check if lake new myproj works

[crab]

it works!

[crab]

thank you!

[Arthur Paulino]

You should be set to open any lean project now, be it Lean 3 or 4

[crab]

tho why is infoview not working? image.png

[Mauricio Collares]

Try opening the HelloWorld folder (and not a .lean file inside it) in VS Code, and then choosing the file you want to edit from the explorer. Alternatively, cd into the HelloWorld folder from the terminal and open VS Code from there. You might need to re-do this if you had it open before running lake new, I'm not sure.

[Mauricio Collares]

Also, did you install the Lean3 or the Lean4 VS Code extension? The correct one for Lean4 is https://marketplace.visualstudio.com/items?itemName=leanprover.lean4

[crab]

Mauricio Collares said:

Try opening the HelloWorld folder (and not a .lean file inside it) in VS Code, and then choosing the file you want to edit from the explorer. Alternatively, cd into the HelloWorld folder from the terminal and open VS Code from there. You might need to re-do this if you had it open before running lake new, I'm not sure.

I did all that

[crab]

Mauricio Collares said:

Also, did you install the Lean3 or the Lean4 VS Code extension? The correct one for Lean4 is https://marketplace.visualstudio.com/items?itemName=leanprover.lean4

I have lean3 extension

[Kevin Buzzard]

Do you want to be using Lean 3 or Lean 4, or don't you know?

[crab]

weird weird image.png

[crab]

Kevin Buzzard said:

Do you want to be using Lean 3 or Lean 4, or don't you know?

lean 4 I think

[Arthur Paulino]

crab said:

Mauricio Collares said:

Also, did you install the Lean3 or the Lean4 VS Code extension? The correct one for Lean4 is https://marketplace.visualstudio.com/items?itemName=leanprover.lean4

I have lean3 extension

The fact that there are two different extensions, one for Lean 3 and another one for Lean 4, makes it a bit confusing to manage.
Try installing the Lean 4 extension and disabling the Lean 3 extension for now.
(Then close and open VS Code again)

[crab]

it worked

[crab]

but why the red underlines? image.png

[Henrik Böving]

true is the bool variant, True the Prop variant, you want True

[Reid Barton]

Alternatively, you want Lean 3.

[Reid Barton]

I'm not really sure how this thread got on the Lean 4 train in the first place.

[Arthur Paulino]

Reid Barton said:

I'm not really sure how this thread got on the Lean 4 train in the first place.

I guess it was just because I'm more familiar with Lean 4 environment, just to test his elan setup. But I wasn't sure if he wanted to learn Lean 4 or Lean 3 either

[Arthur Paulino]

@crab from here it depends on what you want to do. Your setup is working.
Do you want to use mathlib to build something else? Do you want to explore mathlib? Or do you want to learn Lean 4 (which is still at a very WIP stage)?

[crab]

Arthur Paulino said:

crab from here it depends on what you want to do. Your setup is working.
Do you want to use mathlib to build something else? Do you want to explore mathlib? Or do you want to learn Lean 4 (which is still at a very WIP stage)?

i for sure want to use mathlib

[Arthur Paulino]

Then this will help you :)
https://leanprover-community.github.io/install/project.html

[Kevin Buzzard]

mathlib is a lean 3 repo

[crab]

image.png

[Adam Topaz]

@crab did you install mathlibtools? nevermind, I see that you have the leanproject command, which is good.

[Mauricio Collares]

Since you're mainly gonna be using lean3, might as well do elan default leanprover-community/lean:3.35.1. It'll probably fix your problem too.

[Adam Topaz]

I think the issue is that somehow your elan's default lean version is lean4.

[crab]

A new leanproject project doesnt come with default code, right?

[Adam Topaz]

When you use leanproject new foobar, you will get a folder called foobar with no code, but it will contain all of mathlib inside the foobar/_target folder.

[Adam Topaz]

That means you would be able to use mathlib as a dependency.

[Adam Topaz]

Your project's code should go in the foobar/src folder.

[Arthur Paulino]

Also remember to switch your extension back to the Lean 3 one. Sorry for misguiding you into setting up Lean 4. I should have asked your end goal first :+1:

[Mauricio Collares]

But you want samples, you can type leanproject get tutorials to download a separate learning project, for example.

[crab]

Mauricio Collares said:

But you want samples, you can type leanproject get tutorials to download a separate learning project, for example.

thanks!

[crab]

Arthur Paulino said:

Also remember to switch your extension back to the Lean 3 one. Sorry for misguiding you into setting up Lean 4. I should have asked your end goal first :+1:

Its ok!