Worse performance with `lean` than in the editor

Stream: lean4

[Jannis Limperg]

I have a bit of a performance conundrum: an Aesop call which runs quickly (<1s) in the editor but takes a very long time (>30s) when I run lake env lean <testfile>. The culprit seems to be a function which removes certain elements from a DiscrTree which comes from a ScopedPersistentEnvExtension. Before I go on an epic minimisation adventure: any idea where this discrepancy might come from?

[Sebastian Ullrich]

I think I can at least say: no, I have never seen something like that before

[Gabriel Ebner]

I've seen performance differences before, but never to this degree. Like something would time out on the command line, but in the editor you'd need to lower the heartbeats from 200000 to 150000 to get the same exception.

[Jannis Limperg]

Precompilation is somehow implicated in my case: without precompilation, the server and command line are equally slow; with precompilation, the server is much faster.

[Gabriel Ebner]

I think lake env lean doesn't enable precompilation.

[Jannis Limperg]

Nice, I guess that explains it. Now the question is just where this humongous performance difference comes from.

[Jannis Limperg]

Okay, my DiscrTree filtering function was double-accidentally-quadratic. :upside_down: Still unsure where the difference between precompilation and no precompilation comes from, but the immediate problem is solved.

[Sebastian Ullrich]

I'm not sure I understand, if the server used native code but the cmdline used the interpreter, isn't that a sufficient explanation?

[Jannis Limperg]

That is probably the explanation, yes. I'm still a bit unsure because the quadraticness was in the construction of large arrays, which presumably is done with compiled (core) functions in either case. So the only code that would benefit from the compilation would be the skeleton which traverses the DiscrTree, and getting a ~60x speedup from this seems weird. But probably I'm just misunderstanding something.