Gabriel Ebner (May 18 2020 at 16:50):
Since this just came in handy with #2734, there is a semi-useful feature in recent lean versions. If you're working on a file at the beginning of mathlib, and have another file with
import all open, then typically this will cause lots of recompilation. However if you pass the
--old flag to lean, it will use the out-of-date oleans for the files you haven't touched. (This is in settings > Lean: Extra Options)
Bryan Gin-ge Chen (May 18 2020 at 17:02):
Just to make sure I understand, if I start editing a file, even with this option, Lean will never use the oleans for that file, right?
Gabriel Ebner (May 18 2020 at 17:07):
That is the intention. But watch out for bugs.
Sebastien Gouezel (Sep 02 2020 at 11:51):
If I am not mistaken, the option
--old does not show up in
lean --help (but fortunately Zulip is helpful enough to find the name of the option)
Last updated: May 13 2021 at 18:26 UTC