simultaneous compiling + VS Code

Stream: general

[Kevin Buzzard]

Is the following "safe" behaviour:

1) I want to work on latest version of file X in FLT (which has no cache)
2) I git checkout main; git pull; lake exe cache get (for mathlib); lake build FLT/X.lean
3) After compilation of X.lean has finished, I open VS Code, and close all tabs other than X.lean.
4) On the command line I lake build because I may as well build all of FLT as I might need it later on when working on X.lean.

I have absolutely no feeling about whether this sort of behaviour can cause problems. An example of what I'm unsure about: let's say I very quickly decide that I want to now take a look at Y.lean which is not an import of X.lean (e.g. because I want to apply a new result in X to a sorry in Y). Can I just open Y.lean in VS Code and not even care about whether command line compilation has got up to Y.lean yet, or is there some kind of "best practice" I should be sticking to here and this is not it?

[Ruben Van de Velde]

I think you can open Y.lean fine, but I would not make changes to Y.lean or allow it to build its dependencies in parallel with your other lake build. But then maybe lake is smart enough to deal with it

[Mac Malone]

While Lake does nothing to prevent overlapping builds, Lake should generally be robust to them. However, this is not a well-tested aspect of Lake, so some breakage could happen. Nonetheless, I don't think the risk is worth altering your development workflow. Worst case, something goes wrong and you have to clobber .lake and rebuld / re-fetch the cache. Best (and most likely) case, everything just works.

[Mac Malone]

(If something does go wrong, it would also be great to hear about it! It would be nice to make this work consistently.)

[Kevin Buzzard]

I should add that nothing has ever gone wrong for me in the past and it's a habit I'm slowly doing more and more as FLT gets bigger. It just occurred to me that it might not be wise!