Zulip Chat Archive

Stream: general

Topic: manually compiling a dependency


Kevin Buzzard (Apr 20 2019 at 23:00):

Can I use ctrl-C to stop an instance of lean --make running in _target/deps/mathlib when compiling my own mathlib, and then confidently restart the compilation process with lean --make again? On Ubuntu.

Kevin Buzzard (Apr 20 2019 at 23:01):

The code may contain warnings or errors

Chris Hughes (Apr 20 2019 at 23:04):

I do this all the time.

Kevin Buzzard (Apr 20 2019 at 23:05):

Thanks. For someone like you this is a way of getting mathlib to compile if and only if you're not actively working on your computer trying to do other (possibly memory-intensive) tasks.

Kevin Buzzard (Apr 20 2019 at 23:07):

In linux you can just run the task with low priority in the background, and the operating system controls everything for you; all the lean processes swap out and then calm down a lot and basically stop whenever you start using the machine to do anything other than your screensaver

Chris Hughes (Apr 21 2019 at 18:24):

I mainly do it if I'm on a branch I modified, and I make a change.

Chris Hughes (Apr 21 2019 at 18:25):

I never have a problem with background building slowing medown.


Last updated: Dec 20 2023 at 11:08 UTC