Comparing how long it takes to open an empty Lean file

Stream: lean4

[Julian Berman]

I've been doing some light microbenchmarking to try and understand why lean.nvim's test suite takes 30 seconds to run (it does a lot of creating throwaway Lean files). In the process I've been poking at differences in how long it takes to open a Lean file and get a sign from the LSP that Lean is ready to go. I'm not sure I have a real question or point yet but perhaps the below is interesting to someone -- I presume someone more familiar than I am with the details of lake serve's startup will know more precisely what's happening in the startup procedure in each scenario below.

Specifically I timed how long it takes to open a Lean file and have it be ready to go in a few scenarios: 1 as a top level file in a Lean package with fewer dependencies, 2) a standalone file outside of a project 3) as a toplevel file in a project with heavier dependencies (Mathlib) 4) inside of the packages themselves 5) opening an existing file (I picked some random one from lean4export)

Here's the results below:

Time until $/lean/fileProgress says we're done processing our file

⊙  hyperfine --warmup 3 -L file $DEVELOPMENT/Mathlib4/insideProject.lean,$DEVELOPMENT/Mathlib4/Mathlib4/insidePackage.lean,~/Desktop/outsideProject.lean,$DEVELOPMENT/lean4export/fewerDeps.lean,$DEVELOPMENT/lean4export/Export.lean "nvim --cmd 'luafile $DEVELOPMENT/lean.nvim/microbench.lua' {file}"
Benchmark 1: nvim --cmd 'luafile /Users/julian/Development/lean.nvim/microbench.lua' /Users/julian/Development/Mathlib4/insideProject.lean
  Time (mean ± σ):      1.987 s ±  0.212 s    [User: 0.233 s, System: 0.097 s]
  Range (min … max):    1.511 s …  2.165 s    10 runs

Benchmark 2: nvim --cmd 'luafile /Users/julian/Development/lean.nvim/microbench.lua' /Users/julian/Development/Mathlib4/Mathlib4/insidePackage.lean
  Time (mean ± σ):      2.225 s ±  0.038 s    [User: 0.259 s, System: 0.109 s]
  Range (min … max):    2.172 s …  2.291 s    10 runs

Benchmark 3: nvim --cmd 'luafile /Users/julian/Development/lean.nvim/microbench.lua' ~/Desktop/outsideProject.lean
  Time (mean ± σ):      1.115 s ±  0.134 s    [User: 0.213 s, System: 0.085 s]
  Range (min … max):    0.901 s …  1.340 s    10 runs

Benchmark 4: nvim --cmd 'luafile /Users/julian/Development/lean.nvim/microbench.lua' /Users/julian/Development/lean4export/fewerDeps.lean
  Time (mean ± σ):     675.8 ms ±   4.0 ms    [User: 179.5 ms, System: 59.3 ms]
  Range (min … max):   670.2 ms … 682.8 ms    10 runs

Benchmark 5: nvim --cmd 'luafile /Users/julian/Development/lean.nvim/microbench.lua' /Users/julian/Development/lean4export/Export.lean
  Time (mean ± σ):     859.8 ms ±   2.3 ms    [User: 180.9 ms, System: 68.2 ms]
  Range (min … max):   854.2 ms … 862.1 ms    10 runs

Summary
  nvim --cmd 'luafile /Users/julian/Development/lean.nvim/microbench.lua' /Users/julian/Development/lean4export/fewerDeps.lean ran
    1.27 ± 0.01 times faster than nvim --cmd 'luafile /Users/julian/Development/lean.nvim/microbench.lua' /Users/julian/Development/lean4export/Export.lean
    1.65 ± 0.20 times faster than nvim --cmd 'luafile /Users/julian/Development/lean.nvim/microbench.lua' ~/Desktop/outsideProject.lean
    2.94 ± 0.31 times faster than nvim --cmd 'luafile /Users/julian/Development/lean.nvim/microbench.lua' /Users/julian/Development/Mathlib4/insideProject.lean
    3.29 ± 0.06 times faster than nvim --cmd 'luafile /Users/julian/Development/lean.nvim/microbench.lua' /Users/julian/Development/Mathlib4/Mathlib4/insidePackage.lean

If we instead only wait until we start processing a file (i.e. until yellow bars show up), the results on my machine look like:

Time until $/lean/fileProgress says we started processing

⊙  hyperfine --warmup 3 -L file $DEVELOPMENT/Mathlib4/insideProject.lean,$DEVELOPMENT/Mathlib4/Mathlib4/insidePackage.lean,~/Desktop/outsideProject.lean,$DEVELOPMENT/lean4export/fewerDeps.lean,$DEVELOPMENT/lean4export/Export.lean "nvim --cmd 'luafile $DEVELOPMENT/lean.nvim/microbench.lua' {file}"
Benchmark 1: nvim --cmd 'luafile /Users/julian/Development/lean.nvim/microbench.lua' /Users/julian/Development/Mathlib4/insideProject.lean
  Time (mean ± σ):     784.3 ms ± 200.1 ms    [User: 157.5 ms, System: 88.7 ms]
  Range (min … max):   448.8 ms … 1055.8 ms    10 runs

Benchmark 2: nvim --cmd 'luafile /Users/julian/Development/lean.nvim/microbench.lua' /Users/julian/Development/Mathlib4/Mathlib4/insidePackage.lean
  Time (mean ± σ):      1.375 s ±  0.176 s    [User: 0.169 s, System: 0.099 s]
  Range (min … max):    1.142 s …  1.644 s    10 runs

Benchmark 3: nvim --cmd 'luafile /Users/julian/Development/lean.nvim/microbench.lua' ~/Desktop/outsideProject.lean
  Time (mean ± σ):      1.058 s ±  0.056 s    [User: 0.176 s, System: 0.100 s]
  Range (min … max):    0.959 s …  1.123 s    10 runs

Benchmark 4: nvim --cmd 'luafile /Users/julian/Development/lean.nvim/microbench.lua' /Users/julian/Development/lean4export/fewerDeps.lean
  Time (mean ± σ):     713.7 ms ± 120.4 ms    [User: 201.4 ms, System: 101.7 ms]
  Range (min … max):   520.4 ms … 962.2 ms    10 runs

Benchmark 5: nvim --cmd 'luafile /Users/julian/Development/lean.nvim/microbench.lua' /Users/julian/Development/lean4export/Export.lean
  Time (mean ± σ):     892.8 ms ± 172.7 ms    [User: 224.2 ms, System: 120.2 ms]
  Range (min … max):   429.6 ms … 1023.9 ms    10 runs

  Warning: Statistical outliers were detected. Consider re-running this benchmark on a quiet system without any interferences from other programs. It might help to use the '--warmup' or '--prepare' options.

Summary
  nvim --cmd 'luafile /Users/julian/Development/lean.nvim/microbench.lua' /Users/julian/Development/lean4export/fewerDeps.lean ran
    1.10 ± 0.34 times faster than nvim --cmd 'luafile /Users/julian/Development/lean.nvim/microbench.lua' /Users/julian/Development/Mathlib4/insideProject.lean
    1.25 ± 0.32 times faster than nvim --cmd 'luafile /Users/julian/Development/lean.nvim/microbench.lua' /Users/julian/Development/lean4export/Export.lean
    1.48 ± 0.26 times faster than nvim --cmd 'luafile /Users/julian/Development/lean.nvim/microbench.lua' ~/Desktop/outsideProject.lean
    1.93 ± 0.41 times faster than nvim --cmd 'luafile /Users/julian/Development/lean.nvim/microbench.lua' /Users/julian/Development/Mathlib4/Mathlib4/insidePackage.lean

and here there is at least a minor interesting thing to note which is that there is a decent size cost paid when opening a standalone file until lake notices there is no lakefile and falls back to lean --server. Sometimes this is a full second of lost time. Again I'm not sure this is an area of interest but perhaps there's a bit of optimization possible there (e.g. by having the elan wrappers do a quick check for a lakefile before even trying to invoke lake?)

For completeness here's my silly microbenchmark script in case anyone cares to try it:

microbench.lua

local f = io.open("timing", "w")
local t0 = vim.uv.hrtime()
local function log_time(label)
  local elapsed = (vim.uv.hrtime() - t0) / 1e9
  f:write(string.format("%s: %.3f\n", label, elapsed))
  f:flush()
end

vim.api.nvim_create_autocmd("Filetype", {
  pattern = "lean",
  once = true,
  callback = function()
    log_time("Filetype")
  end,
})
vim.api.nvim_create_autocmd("LspAttach", {
  once = true,
  callback = function()
    log_time("lsp is ready")
  end,
})
vim.api.nvim_create_autocmd("User", {
  pattern = "LeanProgressUpdate",
  callback = function()
    local progress = require('lean.progress')
    local current = progress.at(vim.lsp.util.make_position_params(0, 'utf-16'))
    if current == progress.Kind.processing then
      log_time("$/lean/fileProgress processing")
      vim.cmd.quitall()
    else
      log_time("$/lean/fileProgress finished")
    end
  end,
})

(all the actual files in the hyperfine line don't exist on disk, other than Export.lean of course)