Eval's performance

Stream: lean4

[Yuri de Wit]

I have a simple lean program that tries to print the contents of the Environment using #eval, but it is taking a long time.

I understand this is likely a side effect of using the interpreter to eval the expression, but it does sound excessive. So wondering if there is a performance improvement low hanging fruit here.

Here is the #mwe:

import Lean
import Lean.Meta

open Lean Meta

deriving instance Repr for ConstantVal
deriving instance Repr for AxiomVal
deriving instance Repr for ReducibilityHints
deriving instance Repr for DefinitionVal
deriving instance Repr for TheoremVal
deriving instance Repr for OpaqueVal
deriving instance Repr for QuotKind
deriving instance Repr for QuotVal
deriving instance Repr for AxiomVal
deriving instance Repr for InductiveVal
deriving instance Repr for ConstructorVal
deriving instance Repr for RecursorRule
deriving instance Repr for RecursorVal
deriving instance Repr for ConstantInfo

#eval show MetaM _ from do
  let env := (← getEnv)
  env.constants.forM fun n _ => do
    IO.println n

Most of the time it seems to be spent on lean::utf8_strlen():
image.png

And lean::get_utf8_size():
image.png

[Yuri de Wit]

Is there a way I can execute the expression from main to compare it to compiled code?

[Gabriel Ebner]

That might be because it's producing 8 megabytes of text and printing it as error messages is the bottleneck (didn't investigate though). This runs in two seconds (but you need to run it with lean --run so that search paths etc are set up correctly):

import Lean
import Lean.Meta

open Lean Meta

deriving instance Repr for ConstantVal
deriving instance Repr for AxiomVal
deriving instance Repr for ReducibilityHints
deriving instance Repr for DefinitionVal
deriving instance Repr for TheoremVal
deriving instance Repr for OpaqueVal
deriving instance Repr for QuotKind
deriving instance Repr for QuotVal
deriving instance Repr for AxiomVal
deriving instance Repr for InductiveVal
deriving instance Repr for ConstructorVal
deriving instance Repr for RecursorRule
deriving instance Repr for RecursorVal
deriving instance Repr for ConstantInfo

unsafe def main (args : List String) : IO Unit := do
  withImportModules [{module := `Lean}] {} (trustLevel := 1024) fun env =>
    env.constants.forM fun n _ => do
      IO.println n