olean files

Stream: general

[Reid Barton]

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]

No, you need --make as well

[Reid Barton]

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