LeanProfiler

3.5. Close a span only after asynchronous work finishes🔗

An ordinary span stops when its host action returns. That is correct for synchronous work, but a GPU launch or foreign runtime may return while the measured operation is still running. SpanHooks makes the completion rule explicit:

prepare
  start timestamp
    action
    completeTiming
  stop timestamp
enrich
record event

prepare creates adapter state outside the timed interval. completeTiming waits for the work whose completion defines the measurement. enrich runs after the stop timestamp and can attach counters without adding their collection cost to the duration.

let hooks : SpanHooks := {
  State := AsyncToken
  prepare := makeTimingToken
  completeTiming := waitForRuntime
  enrich := fun token metadata => do
    let live ← readLiveBytes token
    pure { metadata with allocLiveBytes := some live }
}

span "foreign.compute" submitWork
  (metadata := {
    backend := some runtimeName
    timing := some "runtime-synchronized"
  })
  (hooks := hooks)

This span measures the host launch path, queue delay, required asynchronous work, and synchronization overhead as one interval. It does not reveal work inside the foreign runtime. Use that runtime's own profiler when the next question lies below the boundary.

Errors from completeTiming and enrich are written to metadata.hookError. They do not replace an exception raised by submitWork. An error from prepare occurs before the event is reserved and returns directly to the caller.