IRExecTrace

IR execution trace viewer (step-by-step evaluation).

TorchLean’s IR semantics (NN.IR.Semantics) can evaluate a graph and either:

• return the full table of intermediate values, or
• stop at the first failure (missing payload, shape mismatch, etc.).

When debugging, it is often more helpful to see:

• which nodes ran successfully,
• the intermediate tensor values (for small graphs),
• and the exact node id where evaluation stopped.

Main commands:

• #ir_exec_trace_view g, input where input : Runtime.AnyTensor α (payload defaults to empty)
• #ir_exec_trace_view g, payload, input where payload : NN.IR.Payload α

Main definitions

• execTrace: execute nodes left-to-right and capture the first failure point.
• irExecTraceHtml: render checks, status badges, and per-node intermediate values.
• #ir_exec_trace_view: command entry point with optional payload.

Implementation notes

• A stop-at-first-failure trace is the default debugging mode for IR execution.
• We intentionally display shape checks next to runtime trace data to reduce context switching.
• This viewer favors explicit node ids and parent links so failures are easy to localize.

References

• ProofWidgets
• GraphViz DOT language
• Lean community documentation style

Tags

ir, execution-trace, debugging, semantics, proofwidgets

def NN.Widgets.irExecTraceHtml {α : Type} [Context α] [Inhabited α] [DecidableEq Spec.Shape] [ToString α] (g : IR.Graph) (payload : IR.Payload α) (input : Runtime.AnyTensor α) : ProofWidgets.Html

Render an "execute and show intermediates" panel for an IR graph and a single input.

Commands

def NN.Widgets.irExecTraceViewCmd1 : Lean.ParserDescr

def NN.Widgets.irExecTraceViewCmd2 : Lean.ParserDescr

def NN.Widgets.«command#ir_exec_trace_view_,_» : Lean.ParserDescr

def NN.Widgets.«command#ir_exec_trace_view_,_,_» : Lean.ParserDescr