## Stream: lean4

### Topic: lean4 repo in vscode

#### Mario Carneiro (Feb 02 2021 at 16:17):

Is it possible to run the vscode-lean4 extension on the lean 4 repo? This was also somewhat subtle in lean 3 because there is no leanpkg.toml file, but it's really useful to explore the code (I imagine Leo & Sebastian use the emacs mode in this repo all the time).

#### Gabriel Ebner (Feb 02 2021 at 16:22):

"Works just fine for me?"

#### Wojciech Nawrocki (Feb 02 2021 at 16:22):

Yes, it should just work if you have elan pointed at a recent lean4. The only difference is for go-to-def, you need to set the LEAN_SRC_PATH environment variable to /path/to/lean4/src.

#### Gabriel Ebner (Feb 02 2021 at 16:22):

Did you run into any issues?

#### Mario Carneiro (Feb 02 2021 at 16:23):

on review it looks like it was the lean 3 extension running instead of lean 4. But after enabling vscode-lean4 in the project, now I'm getting no highlighting or anything, although the file extension is recognized

#### Wojciech Nawrocki (Feb 02 2021 at 16:24):

I observed this too, a workaround is to change language mode to lean4 instead of lean.

#### Marc Huisinga (Feb 02 2021 at 16:25):

You may need to re-open the folder after you set it up so that the extension can launch again

#### Mario Carneiro (Feb 02 2021 at 16:25):

aha, now I have colors but still no errors

#### Marc Huisinga (Feb 02 2021 at 16:27):

vscode-lean4 will yield when the major version of lean is not 4. Does re-opening the folder not work?

#### Mario Carneiro (Feb 02 2021 at 16:27):

how do I control the resolved version of lean without a leanpkg?

#### Mario Carneiro (Feb 02 2021 at 16:28):

lean --version from the root gives Lean (version 3.26.0, commit 5a5c139af3e9, Release)

#### Marc Huisinga (Feb 02 2021 at 16:28):

E.g. by setting lean 4 as your default in elan

...?

#### Wojciech Nawrocki (Feb 02 2021 at 16:29):

You can also run elan override set lean4-toolchain-name in the lean4/ root, but I think that may require you to launch code from that root as well

#### Mario Carneiro (Feb 02 2021 at 16:30):

the only version that shows up in elan toolchain list is leanprover-lean4-4.0.0-m1

#### Wojciech Nawrocki (Feb 02 2021 at 16:31):

That's the initial release? It's quite old, you may want leanprover/lean4:nightly

#### Mario Carneiro (Feb 02 2021 at 16:31):

yeah I know, but I'm not sure where the magic names like leanprover/lean4:nightly are coming from

#### Mario Carneiro (Feb 02 2021 at 16:32):

okay this is working now, thanks folks

#### Mario Carneiro (Feb 02 2021 at 16:33):

although code like this is not getting highlighted right, the comment doesn't end

  /- Generate CodeBlock for doIf; doElems
doIf is of the form

"if " >> optIdent >> termParser >> " then " >> doSeq
>> many (group (try (group (" else " >> " if ")) >> optIdent >> termParser >> " then " >> doSeq))
>> optional (" else " >> doSeq)
  -/
partial def doIfToCode (doIf : Syntax) (doElems : List Syntax) : M CodeBlock := do

#### Gabriel Ebner (Feb 02 2021 at 16:48):

Do we have to set LEAN_SRC_PATH for all lean4 projects now?

#### Sebastian Ullrich (Feb 02 2021 at 16:49):

leanpkg does it automatically when called to build dependencies from the server

#### Mario Carneiro (Feb 02 2021 at 16:50):

It would be nice if there were some vscode setting to override in the lean4 project to make this variable resolve, since I guess a leanpkg.toml isn't an option

#### Mario Carneiro (Feb 02 2021 at 16:51):

(since I guess it is vscode-lean4 that is invoking elan and could set this variable)

#### Sebastian Ullrich (Feb 02 2021 at 16:52):

The only reason we don't have a src/leanpkg.toml is that there is no leanpkg in stage 0 (except with the Nix setup :> ... where it's just a small bash wrapper)

#### Mario Carneiro (Feb 02 2021 at 16:53):

that's not actually a problem though, I think it just means you sometimes have to work without it. For browsing it should be harmless, right?

#### Sebastian Ullrich (Feb 02 2021 at 16:55):

Yes, you're probably correct

Last updated: May 18 2021 at 23:14 UTC