The project is contained inside of another project error

Stream: lean4

[Jakub Nowak]

While working on lean4 I'm having those kind of errors pop-up every time I open new file:

Error while starting language server: The project at '/home/nix/tmp/lean/lean4/src' of the file 'Types.lean' is contained inside of another project at '/home/nix/tmp/lean/lean4', for which a language server is already running. The Lean 4 VS Code extension does not support nested Lean projects.

Although, it seems like everything still works regardless of the error. Anyone knows how to fix the problem?

[Jakub Nowak]

I've used nix develop to get necessary dependencies, build the project with cmake --preset release and make -C build/release -j$(nproc || sysctl -n hw.logicalcpu).
I opened lean.code-workspace with code while it was still building.

Restarting vscode didn't help.

[Marc Huisinga]

Don't create any Lean files at the top-level lean4 directory. All .lean files you create need to be in src or tests. Scratch files go into tests.

[Jakub Nowak]

Ah, yes, I created test.lean file in lean4 directory to test my changes. It seems like moving it to src and restarting vscode helped.

[Marc Huisinga]

You want your test.lean file to be in tests so that it runs with stage1

[Jakub Nowak]

Ah, thanks! You're right, my changes weren't reflected while it was in src directory.

[Kim Morrison]

@Marc Huisinga, I think this one hit me because I opened scripts/AnalyzeGrindAnnotations.lean. That is outside src and tests.

[Marc Huisinga]

Kim Morrison said:

Marc Huisinga, I think this one hit me because I opened scripts/AnalyzeGrindAnnotations.lean. That is outside src and tests.

We could fix this by giving scripts a lean-toolchain file and adding it to the set of workspace folder in core, or we could just accept that when working on this file, we temporarily need to switch between the inner/outer server by clicking the "Stop Other Server" button :-)

[Kim Morrison]

Ah, to clarify, I opened it last week, and don't recall opening it since (and have restarted Code/Cursor several times since).

[Marc Huisinga]

Are you sure that it wasn't open in one of your tabs?

[Kim Morrison]

Yes. :-(

[Marc Huisinga]

Did this occur in Cursor or VS Code?