Multiple tabs in VS Code, shared work?

Stream: lean4

[Joachim Breitner]

I have two mathlib files open in VS Code. After I changed some file in mathlib, I restarted the lean process in both tabs. They are both saying they are recompiling the dependencies, and both say

info: [942/965] Building Mathlib.Data.Real.ENNReal

Am I now building that file twice in parallel, or do lean processes in the same project coordinate somehow (using locking or the like)?

[Joachim Breitner]

It seems all processes are children of a single lean --server, so there seems to be coordination. Also with an additional lake build on the command line?

[Sebastian Ullrich]

There is no locking in Lake yet, no

[Joachim Breitner]

So there is no sharing of dependency rebuilding between two open files in VS Code? Or there is between tabs, but not between manual lake build?

[Sebastian Ullrich]

No sharing at all currently, these are separate lake invocations

[Joachim Breitner]

Ok, thanks! That resolves this thread for me, but I can stop myself from pressing that luring ✓ button :-)