Editing files deep in mathlib

Stream: general

[Chris Hughes]

Whenever I edit files deep inside mathlib, the editor is horribly slow to update, and I have to keep restarting Lean. Is there a way around this?

[Mario Carneiro]

close any other open files

[Mario Carneiro]

and make sure the dependents of the active file are compiled

[Johan Commelin]

Or edit without running Lean... for refactors this sometimes works

[Reid Barton]

or try this --old flag to lean?