Stop lake build after it’s been started by the extension?

Stream: lean4

[Thomas Murrills]

Sometimes I open up a file in VS code that has a lot of deep imports, and suddenly I’m building a thousand files. (This is quite taxing to my laptop.)

I know there’s been discussion about turning this kind of autobuild-on-file-open off, but I wanted to ask about a different thing: is there a way to stop the build without writing killall lake (which stops the server too)? (This might still apply in the non-autobuild case: I deliberately begin the build, realize it’s extensive, then want to interrupt it.)

[Jireh Loreaux]

IIUC, no there isn't (but maybe this has changed in the past month or two).

[Mario Carneiro]

I thought @Sebastian Ullrich had some fix that involved process groups to ensure that killing lake also kills the workers

[Sebastian Ullrich]

And I thought it actually worked since people have stopped complaining (and some did confirm it worked)

[Thomas Murrills]

Hmm, could I be using an old version of lake or lean somehow? What do I need to make sure is up to date to test the new behavior?

[Sebastian Ullrich]

If you work on recent mathlib, that should not be a concern. But you haven't described yet what you actually tried; does closing the file tab not stop the build for you?

[Thomas Murrills]

Oh, I didn’t think to try that! In this case, I wanted to keep looking at the file without building—but that now falls under preventing autobuild, not the issue I brought up here. Closing the file works. Thanks. :)