Slow(er) compilation with large inductive

Stream: lean4

[Yuri de Wit]

I have created a large inductive type with upwards of 260 constructors and noticed slowed compilation times and sluggish VSCode responsiveness (likely a direct consequence). I have since extracted some constructor parameters into separate functions and into different files to get around the problem (it does seem a bit more modular approach anyway). So I am no longer directly impacted by this.

In any case, I am curious as to how the dev team troubleshoots these and what kinds of tools to use (perf seems to be one of these tools and there was another one someone mentioned here recently). I would be happy if I could figure out how to find the hotspot(s) myself.

In addition, let me know if the dev team has any interest in this .lean file and I am happy to share it.

[Sebastian Ullrich]

Yes, perf is always a good idea. Just running perf top while editing a file can already give you a good idea.

[Sebastian Ullrich]

For big inductives specifically, you might want to try set_option genInjectivity false

[Yuri de Wit]

Setting set_option genInjectivity false improves the performance roughly by around 10%.

Here is the perf report without the genInjectivity set:
image.png

This is just running a plain perf record lean myfile.lean. So no priming the pump etc. Let me try to run perf top against the Lean server.

[Yuri de Wit]

Here is a flamegraph based on a DEBUG version of Lean4.

AttributeContent.svg

I cant make much sense of it, but maybe somebody else can.

[Sebastian Ullrich]

Long stack traces are truncated, so it's hard to tell where the replace_rec_fn is coming from. Might be the compiler, which you could test with set_option codegen false

[Sebastian Ullrich]

Though the very first step should probably be running lean with --profile

[Christian Pehle]

I encountered this issue for enum style inductive types here: https://github.com/leanprover/lean4/issues/654, this was then solved with a specialised code path. I think potentially the general case causes has still the same slowdown.

[Sebastian Ullrich]

@Christian Pehle Note, though, https://github.com/leanprover/lean4/commit/70f2200778bd20ab959d8f99ffa32fde4bbfcfe5

[Christian Pehle]

Yes, I didn't find that commit, but as I understood the alternative solution also contains a special case for "enum" like inductive types. There was also a Zulip discussion at the time. But I didn't find it.

[Sebastian Ullrich]

Ah yes, it's the previous commit skipping stage0 updates https://github.com/leanprover/lean4/commit/a7c621854e0f81707ca5c30cf99727b626c394a1

[Yuri de Wit]

This is the result of compiling with --profile with set_option genInjectivity false:

import took 118ms
elaboration took 5.61s
cumulative profiling times:
    elaboration 5.61s
    import 118ms
    initialization 34.4ms
    interpretation 1.43ms
    parsing 5.72ms
    typeclass inference 73.3ms

And with set_option genInjectivity true (close to no real diff):

import took 129ms
elaboration took 5.55s
cumulative profiling times:
    elaboration 5.55s
    import 129ms
    initialization 30.4ms
    interpretation 1.47ms
    parsing 5.96ms
    typeclass inference 68.9ms

This is nowhere near the time documented in https://github.com/leanprover/lean4/issues/654.

Aside from the fact that I am using this as a motivation to learn the compiler etc, the biggest concern would be interactive use cases: it gets annoying fairly quickly. But, that means profiling VSCode + Lean Server instead of this simple batch compilation experiment.

[Sebastian Ullrich]

There shouldn't be any performance difference between the server and batch mode at least