Files open slowly in server mode

[gebner]

Mathlib contains around 3k files. I have made a small stress test to see how long it takes to open a file in the editor with that project size (I was generous, and only generated 1.6k files):

$ time lake print-paths Inundation
{"srcPath":["./."],"oleanPath":["./build/lib"],"loadDynlibPaths":[]}
8.58user 0.89system 0:08.09elapsed 117%CPU (0avgtext+0avgdata 388316maxresident)k
0inputs+25616outputs (0major+24645minor)pagefaults 0swaps

That is, Lake by itself takes more than 8 seconds to find the dependencies and check that they're up to date. This is before Lean can even start to import the oleans and initialize the environment. So a user would need to wait around 10 seconds after opening a file before Lean starts processing the file.

It takes around 8 milliseconds to compute SHA512 hashes for all of the files in that repo. I think that time is a good target for lake print-paths as well.

[Kha]

More comparison (not meant to be a competition, or only a friendly one :) ):

# run Nix' fake lake wrapper after full build
$ nix shell .#lean-dev -c time lake print-paths Inundation
Building dependencies...
{"loadDynlibPaths":[],"oleanPath":["/nix/store/ah8wdmw66asczlcs7avj8wvr3571pw61-print-paths-depRoot"],"srcPath":[".","/nix/store/j37b48sd21xnp9zcv0lhrcmjz0kmsxs1-src","/nix/store/j37b48sd21xnp9zcv0lhrcmjz0kmsxs1-src"]}
0.03user 0.02system 0:00.59elapsed 10%CPU (0avgtext+0avgdata 27332maxresident)k
0inputs+0outputs (0major+3302minor)pagefaults 0swaps

# change unrelated file, forcing Nix' eval cache to miss
$ echo >> README.md; nix shell .#lean-dev -c time lake print-paths Inundation
warning: Git tree '/home/sebastian/Downloads/inundation' is dirty
Building dependencies...
building '/nix/store/47fhdv0igi0l5cqh1z5jms00x3s1ijxb-Inundation-deps.json.drv'...
{"loadDynlibPaths":[],"oleanPath":["/nix/store/ah8wdmw66asczlcs7avj8wvr3571pw61-print-paths-depRoot"],"srcPath":[".","/nix/store/j37b48sd21xnp9zcv0lhrcmjz0kmsxs1-src","/nix/store/j37b48sd21xnp9zcv0lhrcmjz0kmsxs1-src"]}
2.41user 0.83system 0:06.67elapsed 48%CPU (0avgtext+0avgdata 254512maxresident)k
0inputs+624outputs (0major+63634minor)pagefaults 0swaps

# invalidate one file, which makes Nix recompute all dependencies in the package
$ echo >> Inundation.lean; nix shell .#lean-dev -c time lake print-paths Inundation
Building dependencies...
building '/nix/store/mwjqg5ng34qdng6kwg31shf6wfqbam8x-Inundation-deps.json.drv'...
these 3 derivations will be built:
  /nix/store/jqy3xj3nf22hxi9mwwqqxznsb6rp4z99-Inundation.drv
  /nix/store/irisrcgkcykglqbwy1fmym3chl19chj7-print-paths-depRoot.drv
  /nix/store/a370xhfswiayk659jbpjz702ffqgg933-print-paths.drv
building '/nix/store/jqy3xj3nf22hxi9mwwqqxznsb6rp4z99-Inundation.drv'...
building '/nix/store/irisrcgkcykglqbwy1fmym3chl19chj7-print-paths-depRoot.drv'...
building '/nix/store/a370xhfswiayk659jbpjz702ffqgg933-print-paths.drv'...
{"loadDynlibPaths":[],"oleanPath":["/nix/store/8b2ywafx5q4mqc2f6mm6s3hapcl2q2hh-print-paths-depRoot"],"srcPath":[".","/nix/store/j37b48sd21xnp9zcv0lhrcmjz0kmsxs1-src","/nix/store/j37b48sd21xnp9zcv0lhrcmjz0kmsxs1-src"]}
2.07user 0.68system 0:07.33elapsed 37%CPU (0avgtext+0avgdata 254876maxresident)k
0inputs+592outputs (0major+63646minor)pagefaults 0swaps

So not exactly better except in the ideal case 🤔 ...

[gebner]

Thanks! This is very interesting. So Nix's advantage is really mostly due to the flake eval cache!

For comparison, could you also post how long lake print-paths Inundation takes on your machine?

[tydeu]

@Kha So, according to @gebner's results, this implies that Lake has a 3-4x overhead over Nix (w/o the cache). How much of that do you think is likely just due to the differences in language and codegen of Lean?

[gebner]

this implies that Lake has a 3-4x overhead over Nix (w/o the cache). How much of that do you think is likely just due to the differences in language and codegen of Lean?

I'm not sure where you see the 3-4x overhead here, both Lake and Nix (without eval cache) take around 8 wallclock seconds for a build. (Note that Nix has a daemon, so don't read too much into the user time.)

For Lake, I think the (lack of) performance has nothing to do with the Lean compiler or using Lean as the programming language. Most of the issues seem to be architectural or algorithmic. See for example the accidentally quadratic computation of imports fixed by #132.

[tydeu]

@gebner

I'm not sure where you see the 3-4x overhead here, both Lake and Nix (without eval cache) take around 8 wallclock seconds for a build. (Note that Nix has a daemon, so don't read too much into the user time.)

I was an idiot and read the user time as wall clock time instead of noting the elapsed time.

Most of the issues seem to be architectural or algorithmic.

Yeah, I definitely know there are no doubt problems with that. My originally question (which is now essentially moot due to actual difference being smaller than I though) was simply what percent of overhead, if any, should one expect from code written in Lean versus something written in a language like Nix (or vice versa).

[gebner]

My originally question (which is now essentially moot due to actual difference being smaller than I though) was simply what percent of overhead, if any, should one expect from code written in Lean versus something written in a language like Nix (or vice versa).

Your question is moot, but for very different reasons. Namely that Nix comes built-in with a very different architecture. At a very high level, you send shell scripts together with a list of dependencies to the Nix daemon. That daemon will run the shell script in a sandbox with only the dependencies visible. But only the first time, after that it is cached. The result of the shell script is identified by a hash of the shell scripts and the list of dependencies. Sebastian's Nix integration essentially produces one shell script per olean/o/etc. file. From what I can tell, a lot of the overhead comes from producing the shell scripts, spawning a sandbox for every program call, copying the source code into the store, and general bookkeeping (Nix uses an actual SQL database to keep track of the build results). None of which has anything to do with Nix the language.

On a language level, Lean is lightyears ahead of Nix. (Unless you really want to do lazily evaluated dictionaries that cyclically depend on themselves.)

[gebner]

After #132, the biggest cost centers are Lean.Elab.parseImports (22%), computeFileHash (17%), and loading the lakefile (14%).

[gebner]

Oooh, there are some low-hanging fruit in Lean.Elab.parseImports. We actually initialize a new empty environment every single time we parse the imports....

[tydeu]

@gebner

After #132, the biggest cost centers are Lean.Elab.parseImports (22%)

Oh I didn't realize parseImports was that slow. If that remains the case, making it into an asynchronous job may help save time in Lake (as we can parse the imports of multiple files simultanously).

[tydeu]

@Kha I believe you were the one who setup benchmarking on the Lean 4 repository. Any chance you can advise me how I could do the same here on Lake? It would be able to use automagically use performance tests like @gebner's to benchmark PRs, commits, and the like.

[Kha]

For comparison, could you also post how long lake print-paths Inundation takes on your machine?

Right, it's 10s for Lake (without your change). It's a laptop.

[Kha]

@Kha I believe you were the one who setup benchmarking on the Lean 4 repository. Any chance you can advise me how I could do the same here on Lake?

Unfortunately the setup is a bit bespoke, I think we need a separate benchmarking machine per repo... it's also not clear where the infrastructure will go after I finish my PhD.

[tydeu]

@Kha ah 😞 -- do you have any advice on alternative solutions for GitHub benchmarking then? -- a quick search turned up the Continuous Benchmark action, but I, unfortunately, do not have much experience on what to look for in this area.

[Kha]

As far as watching the benchmark results of examples in this repository, the amplitude of the benchmarks is about +- 10~20%.

That does not bode well for benchmarking on GitHub Actions

[tydeu]

After #132, the biggest cost centers are Lean.Elab.parseImports (22%), computeFileHash (17%), and loading the lakefile (14%).

With the old addition of parseImports', and the new file hash caching (lean4#2444) and precompiled oleans (lean4#2480), all these major cost centers should be addressed. The Inundation benchmark will also be in lean4#2457. Thus, I am closing this issue.

[digama0]

What are the performance numbers and breakdown now?

[tydeu]

@digama0 As the benchmark machine is not Gabriel's or Sebastian's, we do not have exactly comparable benchmarks. However, this analysis compares the benchmarks before and after the new changes (where lake build dummy is the Inundation build). I currently do not use Inundation for the no-op build, because it is not as useful as a no-op Lean build (because the modules in Inundation do not have real code and thus things like the hashing optimization do not produce significant results). I also suspect that the crlf2lf change already substantially reduced the hashing time.

[tydeu]

@digama0 It is also worth noting that hashing optimization only significantly impacted the task-clock, not the wall-clock time. Lake is already very efficient at hashing files with its massive parallelism as Sebastian's Hotspot analysis showed. However, on machines with few threads/cores it is a major benefit. It may also help downstream project's like cache use the hashes rather than hashing themselves.