LeanProfiler

1.3. Time work, not a lazy value🔗

span accepts an IO action. That boundary matters because a pure value can remain partly unevaluated until a later action prints, stores, or passes it to foreign code. Put the span around the action that actually forces the work.

The profiled def syntax keeps a small IO function concise:

profiled def loadBatch : IO Unit := do
  IO.sleep 2

Use an explicit span when the same function needs different names or metadata at different call sites.