Opening a file in core gives lots of errors

Stream: lean4

[Bhavik Mehta]

Opening Lean/Elab/Tactic/RCases.lean gives me a ton of errors from a project on 4.18.0-rc1, starting on line 68:

elaboration function for 'Lean.Elab.Tactic.RCases.termListΠ._@.Lean.Elab.Tactic.RCases._hyg.538' has not been implemented
  ListΠ

@Kevin Buzzard reports seeing the same thing from mathlib on v4.15.0-rc1, and also from mathlib master on v4.19.0-rc2. What's going on here?

[Edward van de Meent]

The specific notation this is referring to looks to be defined at around line 30 of the same file...

[Kevin Buzzard]

So just to be clear, I've got mathlib open and then I'm opening some file in ~/.elan/toolchains so in particular it's not within the project.

[Eric Wieser]

What does lean --version give when run from that directory?

[Kevin Buzzard]

I'm not at Lean right now but I got to the file via "jump to definition"

[Bhavik Mehta]

Likewise for me, and the jump to definition was from a file in (working) mathlib

[Eric Wieser]

I suspect the answer is that elan doesn't know which lean to run

[Eric Wieser]

And so it uses whatever your default toolchain is

[Bhavik Mehta]

Shouldn't it be the same Lean server that's already running in mathlib? It's the same vscode window

[Eric Wieser]

No, you can have multiple servers within the same window

[Eric Wieser]

Vscode just asks elan to choose a lean version for whatever directory it is looking at

[Bhavik Mehta]

When in ~/.elan/toolchains/leanprover--lean4---v4.18.0-rc1, I get

$ lean --version
Lean (version 4.18.0-rc1, x86_64-apple-darwin22.6.0, commit 69a1d0485e24, Release)

[Eric Wieser]

What about in the exact folder where the .lean file you're looking at is?

[Bhavik Mehta]

Exactly the same result

[Kyle Miller]

Does elan override list show anything?

[Bhavik Mehta]

/Users/bmehta/Documents/lean/mathport/Oneshot/lean3-in  leanprover-community/lean:3.51.1
/Users/bmehta/Documents/lean/mathport/sources/lean      leanprover-community/lean:3.51.1

[Bhavik Mehta]

Kevin might be able to give better debug information, his laptop is fast and clean and mine is old and has a bunch of crap on it :)