Zulip Chat Archive

Stream: new members

Topic: slow CL execution/imports


view this post on Zulip Logan Murphy (Nov 03 2020 at 18:40):

I have a Lean program being called from command line, and I'm finding that it's pretty slow to respond, which I assume is because I have several files being imported in the main file and each has to be compiled/checked at runtime. What should I do to speed this up? Is this what olean files are for? Or are there other things I should do?

view this post on Zulip Rob Lewis (Nov 03 2020 at 18:41):

Yes, that's what olean files are for. Run lean --make main.lean to compile them.

view this post on Zulip Logan Murphy (Nov 03 2020 at 18:42):

Great, thanks Rob!


Last updated: May 14 2021 at 03:27 UTC