performance difference between `lake exec` vs `#eval`

Stream: lean4

[Alexandre Rademaker]

I am working with an algorithm that needs to read some text files. I noticed a substantial difference in the performance of executing the same function when called from the command line lake exec versus when I tested it using #eval. Is this expected?

[Arthur Paulino]

I think so. lake exec is summoning the whole compilation pipeline, producing C code and compiling it to an executable binary.