IR execution trace

#ir_exec_trace_view g, input evaluates nodes in order and displays intermediate values until the first evaluation error. The input is Spec.SomeTensor α; an explicit NN.IR.Payload α can be supplied with #ir_exec_trace_view g, payload, input instead of the empty default.

irExecTraceHtml reports well-formedness and shape checks separately from evaluation. A failed check does not prevent the panel from attempting a trace. Displaying a result does not prove it.

def NN.Widgets.irExecTraceHtml {α : Type} [TorchLean.Storage α] [Context α] [ToString α] (g : IR.Graph) (payload : IR.Payload α) (input : Spec.SomeTensor α) : 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