Zulip Chat Archive

Stream: lean4

Topic: Navigating the core library

Floris van Doorn (Oct 23 2024 at 22:30):

Is there a way to navigate the Lean core library in VSCode, with Lean interpeting these files without error?

  • If I am in a separate repo and open a file from Core (say Lean.Expr) I get the error
unknown package 'Std'
You might need to open 'c:\Users\Floris\.elan\toolchains\leanprover--lean4---v4.13.0-rc3\src\lean' as a workspace in your editor
  • If I open that folder as a workspace, I get the same error
  • If I checkout the Lean4-repo at the v4.13.0-rc3 branch I get some scary errors. This also contains the output of elan --show (with weird errors)

long output

Floris van Doorn (Oct 23 2024 at 22:34):

(note: if I checkout the Lean 4 repo at a commit from ~1 year ago, it works just fine in VSCode)

Floris van Doorn (Oct 23 2024 at 22:43):

Oh, I guess this related to the latest release candidate, so feel free to ignore this if this is WIP. It works fine on Lean from 1 month ago.

Eric Wieser (Oct 23 2024 at 22:53):

I think this is because when you open the lean folder, elan just uses a random lean toolchain

Eric Wieser (Oct 23 2024 at 22:53):

And so the fix is to set the default elan toolchain to the same version as the source you're looking at

Floris van Doorn (Oct 23 2024 at 22:58):

I did try to look at the v4.13.0-rc3 branch with the same default toolchain, which also didn't work.

It might have to do with the fact that Core has been split into Lean + Std recently?

Kim Morrison (Oct 24 2024 at 06:00):

Have you followed the instructions at https://lean-lang.org/lean4/doc/dev/index.html#dev-setup-using-elan

Kim Morrison (Oct 24 2024 at 06:00):

in particular about creating the toolchains?

Floris van Doorn (Oct 24 2024 at 07:45):

I have not. I am also not trying to change Lean Core, just navigate the existing code without errors, so I was not aware that that page was relevant for me.

Sebastian Ullrich (Oct 24 2024 at 08:16):

When I Ctrl+click on e.g. import Lean.Expr in Mathlib.Lean.Expr.ReplaceRec, everything works for me and "Lean 4: Troubleshooting: Show Setup Information" says

...
Elan: Reasonably up-to-date (version: 3.1.1)
Lean: Reasonably up-to-date (version: 4.13.0-rc3)
Project: Valid Lean project (path: /home/sebastian/.elan/toolchains/leanprover--lean4---v4.13.0-rc3/src/lean)

active toolchain

leanprover/lean4:v4.13.0-rc3 (override because inside toolchain directory '/home/sebastian/.elan/toolchains/leanprover--lean4---v4.13.0-rc3')

Lean (version 4.13.0-rc3, x86_64-unknown-linux-gnu, commit 01d414ac36dc, Release)

Last updated: May 02 2025 at 03:31 UTC