Using out-of-date oleans without recompiling

Stream: general

[Gabriel Ebner]

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]

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]

That is the intention. But watch out for bugs.

[Sebastien Gouezel]

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)