VSCode extension: multiple Lake packages in a repository

Stream: general

[pandaman]

Recently, I moved the correctness proofs in my library into a separate Lake package in a subdirectory like this (repo):

lean-regex
├ lakefile.toml # Implementation package without any dependencies
├ Regex.lean    # Root of the implementation
└ correctness
     ├ lakefile.toml         # Package for correctness proofs
     └ RegexCorrectness.lean # Root of the proofs

The lake commands work without issues when running at the repository root/in the correctness directory, but I found that the VSCode extension only recognizes packages declared in the root lakefile.toml. In other words, when I opened a file in correctness from a VSCode (launched at the repository root), I got an error like this:

unknown module prefix 'RegexCorrectness'

No directory 'RegexCorrectness' or file 'RegexCorrectness.olean' in the search path entries:
././.lake/build/lib
././.lake/build/lib
/path/to/.elan/toolchains/leanprover--lean4---v4.16.0-rc2/lib/lean
/path/to/.elan/toolchains/leanprover--lean4---v4.16.0-rc2/lib/lean

I could work this issue around by opening a separate VSCode at the correctness directory, but it's a bit inconvenient to switch between two VSCode windows. Is there any way to make the VSCode extension work seamlessly between the two packages in a repository?

[Marc Huisinga]

Nested Lake packages are currently not supported by the VS Code extension due to a limitation of the VS Code language client library.

[Marc Huisinga]

What should however work is having one top-level repository that contains multiple disjoint Lake projects.

[pandaman]

Thanks! Do you know if Reservoir can find it if I move Regex.lean and its lakefile.toml into a separate directory as well (assuming disjoint Lake project means this)?

[pandaman]

Looks like no: https://github.com/leanprover/reservoir/issues/13

[pandaman]

Separating all Lake packages into individual directories fixed the issue. Thanks!

Lake seems to have a notion of workspace as a collection of packages, so I hope I can use it to group my packages and Reservoir recognize them in the future.