slow CL execution/imports

Stream: new members

[Logan Murphy]

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]

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

[Logan Murphy]

Great, thanks Rob!