## Stream: general

### Topic: olean files

#### Reid Barton (Sep 06 2018 at 17:49):

If I invoke lean on a single file like lean src/category_theory/rel.lean, then it should write out an .olean file if it finishes and succeeds, right? (Let's say there is no existing .olean file to start with.)

#### Sebastian Ullrich (Sep 06 2018 at 17:50):

No, you need --make as well

#### Reid Barton (Sep 06 2018 at 17:53):

Oh okay. Well that's one mystery solved.
I still have a situation where leanpkg build is doing a build which is running out of memory, but I'm pretty sure it has finished building a lot of other files first, and it's not writing .olean files for them. But I should at least be able to work around that now

Last updated: May 10 2021 at 00:31 UTC