mathlib3 in separate window

Stream: mathlib4

[Joachim Breitner]

The wiki says it’s recommended to open the mathlib3 in a separate VScode window, but it seems that lean4 tries to process it. Is there a trick?

[Kevin Buzzard]

This works fine for me. You're opening the root directory of the mathlib3 repo using "open folder" and you have the lean3 extension installed?

[Joachim Breitner]

I ran code path/to/file, which probably isn't the same as opening a folder. Thanks, will try that!

[Johan Commelin]

Yeah, you need to use code path/to/root and then open the file in VScode