feat: lake: save elaborated config as an olean

[tydeu]

Local benchmarks indicate that this does not have much effect on simple configurations, but has a major impact on complex ones. For instance, using an prebuilt OLean gave a ~5x configuration speedup for the FFI example on my machine. Essentially, it makes configure time near constant, rather than directly proportional to the complexity of the configuration.

The limiting factor for simple configurations appears to be that the initial import of Lake is still expensive.

[tydeu]

While I would like a review, merging should wait until this is tested against benchmarks like #2457.

[tydeu]

!bench

[leanprover-bot]

Here are the benchmark results for commit fda7e93.
There were no significant changes against commit a7efe5b.

[tydeu]

Comparing this benchmark with the plain one in #2457 (comment) displays the expected significant improvement to configuration time. From the comparison:

  Benchmark         Metric         Change
  =================================================
+ lake build no-op  branch-misses  -12.1% (-16.4 σ)
+ lake build no-op  branches       -9.3% (-35.4 σ)
+ lake build no-op  instructions   -7.5% (-28.2 σ)
+ lake configure    branch-misses  -79.5% (-217.3 σ)
+ lake configure    branches       -70.7% (-990.4 σ)
+ lake configure    instructions   -70.9% (-783.7 σ)
+ lake configure    maxrss         -7.5% (-16.5 σ)
+ lake configure    task-clock     -52.4% (-34.7 σ)
+ lake configure    wall-clock     -52.6% (-35σ)

[kim-em]

On Mathlib master, lake env currently takes 1.72s.

On the toolchain leanprover/lean4-pr-releases/pr-release-2480:

• without a lakefile.olean present lake env takes 1.05s, or
• with a lakefile.olean present lake env takes 0.91s

[tydeu]

@semorrison

On Mathlib master, lake env currently takes 1.72s.
without a lakefile.olean present lake env takes 1.05s
with a lakefile.olean present lake env takes 0.91s

This is surprising. I am not sure why the configuration without the OLean would have gotten significantly faster. Similarly, I am surprised the OLean only gave an ~10% boost.

When you ran the test without the OLean, did you run it in fresh repository or did you just delete the lakefile.olean? If the latter, the difference may be due to the lakefile.olean files still remaining in dependencies (e.g., proofwidgets). Instead of deleting files, you can use the -R option to force Lake to re-elaborate the configuration from the source.

[kim-em]

That was it. Now I get (averaging 10 runs each):

• pre feat: lake: save elaborated config as an olean #2480, lake env takes 1.72s
• post feat: lake: save elaborated config as an olean #2480, lake env -R takes 2.15s
• post feat: lake: save elaborated config as an olean #2480, lake env takes 0.89s

Is the slowdown with -R expected?

[tydeu]

@semorrison Yes, Lake now just memoizes the import state, not the full environment (because that environment cannot be used by the cached oleans), so there is some expected overhead from recreating it for each dependency.

EDIT: I did not feel it was worth it to also cache the environment on top of that because it would would only be useful for -R, which hopefully will not be commonly used, so the overhead is acceptable.

[tydeu]

@semorrison One thing I am curious about from your numbers. How fast is lake self-check on the machine you were running these benchmarks on? That gives a good startup baseline for Lake to see how much room there is to improve.

[kim-em]

lake self-check is taking 0.08s.

[tydeu]

@semorrison

lake self-check is taking 0.08s.

Wow! That is also a much greater difference between startup and configure times than the speed center benchmark. As such, I would curious in a more fine-grained profile of the Lake's performance in mathlib after merging all these performance improvements. That is, using something like Hotspot (like Sebastian's previous analysis).