RuntimeCtx

Runtime context viewer widget (variables + gradients).

When stepping through a training loop, the most common debugging questions are:

• Which parameters exist and what shapes do they have?
• Which variables have gradients, and do their shapes match the corresponding values?

This widget renders Runtime.RuntimeContext as two tables:

• var_registry (values),
• gradients (accumulated gradients).

Main definitions

• runtimeCtxHtml: top-level context renderer.
• sectionHtml: reusable expandable section builder.
• kvRow: per-variable row with tensor preview.
• #runtime_ctx_view: command entry point.

Implementation notes

• We split variables and gradients into separate sections because that mirrors how people debug training state ("what exists?" vs "what got grad?").
• Expanded rows show tensor previews directly, which helps identify shape issues without leaving the infoview.
• This viewer is intentionally read-only and does not mutate runtime state.

References

• ProofWidgets
• Lean community documentation style

Tags

runtime-context, gradients, variables, debugging, proofwidgets

def NN.Widgets.runtimeCtxHtml {α : Type} [ToString α] (ctx : Runtime.RuntimeContext α) : ProofWidgets.Html

Render a runtime context as a rich HTML panel.

Commands

def NN.Widgets.runtimeCtxViewCmd : Lean.ParserDescr

def NN.Widgets.«command#runtime_ctx_view_» : Lean.ParserDescr