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.