Zulip Chat Archive

Stream: general

Topic: Using out-of-date oleans without recompiling

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: Dec 20 2023 at 11:08 UTC