Pre-release testing for nested Lean project support in VSC

Stream: lean4

[Marc Huisinga]

Pre-release 0.0.222 of the Lean 4 VS Code extension has support for using the extension in nested Lean projects, i.e. Lean projects with a top-level lean-toolchain file and then somewhere in that project tree another Lean project with its own lean-toolchain file.
The outer language server will now manage all Lean files except those in the nested project, which are managed by an inner language server.

The implementation of this new feature is a bit tricky, so I would be very grateful if people could try out 0.0.222 before we release these changes to everyone. I'm especially curious about any non-default Lean project setups that already worked fine previously.

You can install the pre-release by navigating to the 'Extensions' side bar menu, selecting the 'Lean 4' extension and clicking the 'Switch to Pre-Release Version' button. You may also need to click 'Update' in the extension menu afterwards and restart VS Code (or just the extension host).
Installing pre-releases

Thanks!

[Patrick Massot]

I know this is not really related but the nesting makes me think of a big wish list item for 2026: it would be really fantastic if lake build could search for a lakefile in parents folders. It’s a really common frustration to read error: [root]: no configuration file with a supported extension: every time I type lake build in my library folder, one level deeper than my lakefile.toml.

[Kevin Buzzard]

Great to see that I'm not the only person doing this ;-) It even says I'm in directory FLT, but it turns out that it's FLT/FLT :-)