Zulip Chat Archive

Stream: general

Topic: olean files


view this post on Zulip 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.)

view this post on Zulip Sebastian Ullrich (Sep 06 2018 at 17:50):

No, you need --make as well

view this post on Zulip 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