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 optional profiled def syntax keeps a small IO function concise. It has its own import because defining a command requires Lean's compiler front end:

import LeanProfiler.Syntax

open LeanProfiler

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

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