Documentation

Lean.Elab.Idbg

Interactive Debug Expression Evaluator (idbg) #

idbg enables live communication between a running compiled Lean program and the language server.

Protocol #

Communication uses a length-prefixed TCP protocol over localhost. Both server (language server side) and client (compiled program side) compute a deterministic port from the source location hash.