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: May 14 2021 at 03:27 UTC