Zulip Chat Archive

Stream: new members

Topic: slow CL execution/imports

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?

Rob Lewis (Nov 03 2020 at 18:41):

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

Logan Murphy (Nov 03 2020 at 18:42):

Great, thanks Rob!

Last updated: Dec 20 2023 at 11:08 UTC