Zulip Chat Archive

Stream: general

Topic: Editing files deep in mathlib


view this post on Zulip Chris Hughes (May 27 2020 at 12:32):

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?

view this post on Zulip Mario Carneiro (May 27 2020 at 12:33):

close any other open files

view this post on Zulip Mario Carneiro (May 27 2020 at 12:33):

and make sure the dependents of the active file are compiled

view this post on Zulip Johan Commelin (May 27 2020 at 12:35):

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

view this post on Zulip Reid Barton (May 27 2020 at 12:45):

or try this --old flag to lean?


Last updated: May 17 2021 at 21:12 UTC