Any chance to have compiled-level speed in interactive mode?

Stream: lean4

[Qiyuan Zhao]

I am writing some computationally intensive functions in Lean. I have noticed a significant performance gap between running the code in interactive mode (e.g., via #eval) and running the compiled binary (e.g., first lake build and using the binary). I assume this is because interactive mode relies on the interpreter, whereas the binary is compiled from the C IR.

Is there any way to achieve performance comparable to the compiled binary while staying in interactive mode? I need real-time feedback with these functions. If compiled-level performance isn't achievable directly in the editor, I would have to resort to ad-hoc workarounds, such as implementing a custom command that compiles a temporary file in the background, executes the function externally, fetches the result through RPC and displays it.

Any advice or better approaches would be greatly appreciated. Thanks!

[Henrik Böving]

You can in principle use the precompileModules feature in your lakefile to natively compile your library even for interactive use.

[Qiyuan Zhao]

Thanks for the reply!

Indeed, precompileModules speeds up code that is fully contained within the library. However, my situation is slightly more complex: my library functions are higher-order, and they need to accept functions defined in the current interactive session as arguments. In this scenario, precompileModules seems to have limited effectiveness.

Here is a minimal example to illustrate (my Lean version is v4.25.2):

In Mini.lean (the library):

def isPrime' (n : Nat) (f : Nat → Bool) : Bool := Id.run do
  if n < 2 then false
  else
    for i in [2:n] do
      if i * i > n then break
      if f i then return false
    return true

def isPrime (n : Nat) : Bool := isPrime' n (n % · == 0)

In Main.lean (interactive use):

import Mini

def main (xs : List String) : IO Unit := do
  let n := xs[0]?.bind String.toNat?
  match n with
  | some num =>
    -- let b := isPrime num  -- Case A
    let b := isPrime' num (num % · == 0)  -- Case B
    let res := if b then "is a prime number." else "is not a prime number."
    IO.println s!"{num} {res}"
  | none =>
    IO.println "Please provide a valid natural number."

#time #eval main ["29996224275833"]

Without precompileModules on Mini, both Case A (isPrime) and Case B (isPrime') take around 2.5s. With precompileModules enabled, Case A drops to around 0.1s and Case B only drops to around 1s. In my actual application, I am constrained to the "Case B" pattern (i.e., the logic passed as an argument is dynamic and cannot be defined in the library beforehand).

Is there any way to mitigate this specific situation?

[Henrik Böving]

Well it does already work, the issue is just that there is a closure call back into the interpreter. I don't think you can work around that at the moment