lean4 repo in vscode

Stream: lean4

[Mario Carneiro]

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]

"Works just fine for me?"

[Wojciech Nawrocki]

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]

Did you run into any issues?

[Mario Carneiro]

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]

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

[Marc Huisinga]

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

[Mario Carneiro]

aha, now I have colors but still no errors

[Marc Huisinga]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Marc Huisinga]

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

[Mario Carneiro]

...?

[Wojciech Nawrocki]

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]

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

[Wojciech Nawrocki]

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

[Mario Carneiro]

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

[Mario Carneiro]

okay this is working now, thanks folks

[Mario Carneiro]

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
    let view ← liftMacroM $ mkDoIfView doIf
    let thenBranch ← doSeqToCode (getDoSeqElems view.thenBranch)
    let elseBranch ← doSeqToCode (getDoSeqElems view.elseBranch)
    let ite ← mkIte view.ref view.optIdent view.cond thenBranch elseBranch
    concatWith ite doElems

[Mario Carneiro]

I guess that's an issue with the vscode syntax highlighter in both lean 3 and lean 4

[Sebastian Ullrich]

Updated instructions: https://github.com/leanprover/lean4/commit/f80147e264c30f6409be5eb2f3f74f0912917ebc (though this still assumes local development, not just browsing)

[Marc Huisinga]

oh yeah, that's broken

[Mario Carneiro]

When you say to open src/ as workspace folder, do you mean that the project root should be src or that it should be a two-folder workspace with both lean4/ and lean4/src open?

[Mario Carneiro]

Ooh, go to definition + hovers = :rainbow:

[Sebastian Ullrich]

Mario Carneiro said:

When you say to open src/ as workspace folder, do you mean that the project root should be src or that it should be a two-folder workspace with both lean4/ and lean4/src open?

I believe the only important part is that you do not open only the root as a workspace since then elan will be called from there and use the wrong stage. Which doesn't matter for browsing of course.

[Gabriel Ebner]

I have set an elan override for lean4/ and then open code lean4/. This also works fine.

[Mario Carneiro]

that's what I did at first but go to definition didn't work

[Mario Carneiro]

opening src works but then you can't see the whole project

[Gabriel Ebner]

Go-to-definition works for me as well (after setting LEAN_SRC_PATH).

[Mario Carneiro]

Do I have to invoke LEAN_SRC_PATH=lean4/src code lean4/ to make that work?

[Mario Carneiro]

or did you just stick that in your bashrc or something

[Gabriel Ebner]

I used the absolute path, env LEAN_SRC_PATH=$PWD/src code .

[Gabriel Ebner]

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

[Sebastian Ullrich]

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

[Mario Carneiro]

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]

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

[Sebastian Ullrich]

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]

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]

Yes, you're probably correct