Zulip Chat Archive

Stream: lean4

Topic: lean4 repo in vscode


view this post on Zulip 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).

view this post on Zulip Gabriel Ebner (Feb 02 2021 at 16:22):

"Works just fine for me?"

view this post on Zulip 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.

view this post on Zulip Gabriel Ebner (Feb 02 2021 at 16:22):

Did you run into any issues?

view this post on Zulip 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

view this post on Zulip Wojciech Nawrocki (Feb 02 2021 at 16:24):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 02 2021 at 16:25):

aha, now I have colors but still no errors

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Feb 02 2021 at 16:27):

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

view this post on Zulip Mario Carneiro (Feb 02 2021 at 16:28):

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

view this post on Zulip Marc Huisinga (Feb 02 2021 at 16:28):

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

view this post on Zulip Mario Carneiro (Feb 02 2021 at 16:28):

...?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Wojciech Nawrocki (Feb 02 2021 at 16:31):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 02 2021 at 16:32):

okay this is working now, thanks folks

view this post on Zulip 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
    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

view this post on Zulip Mario Carneiro (Feb 02 2021 at 16:34):

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

view this post on Zulip Sebastian Ullrich (Feb 02 2021 at 16:34):

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

view this post on Zulip Marc Huisinga (Feb 02 2021 at 16:34):

oh yeah, that's broken

view this post on Zulip Mario Carneiro (Feb 02 2021 at 16:36):

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?

view this post on Zulip Mario Carneiro (Feb 02 2021 at 16:39):

Ooh, go to definition + hovers = :rainbow:

view this post on Zulip Sebastian Ullrich (Feb 02 2021 at 16:42):

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.

view this post on Zulip Gabriel Ebner (Feb 02 2021 at 16:43):

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

view this post on Zulip Mario Carneiro (Feb 02 2021 at 16:44):

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

view this post on Zulip Mario Carneiro (Feb 02 2021 at 16:44):

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

view this post on Zulip Gabriel Ebner (Feb 02 2021 at 16:46):

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

view this post on Zulip Mario Carneiro (Feb 02 2021 at 16:46):

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

view this post on Zulip Mario Carneiro (Feb 02 2021 at 16:47):

or did you just stick that in your bashrc or something

view this post on Zulip Gabriel Ebner (Feb 02 2021 at 16:47):

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

view this post on Zulip Gabriel Ebner (Feb 02 2021 at 16:48):

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

view this post on Zulip Sebastian Ullrich (Feb 02 2021 at 16:49):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 02 2021 at 16:51):

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

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip Sebastian Ullrich (Feb 02 2021 at 16:55):

Yes, you're probably correct


Last updated: May 18 2021 at 23:14 UTC