manually compiling a dependency

Stream: general

[Kevin Buzzard]

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]

The code may contain warnings or errors

[Chris Hughes]

I do this all the time.

[Kevin Buzzard]

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]

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]

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

[Chris Hughes]

I never have a problem with background building slowing medown.