feat: idbg interactive debug expression evaluator (#12648)
This PR adds the experimental `idbg e`, a new do-element (and term) syntax for live debugging between the language server and a running compiled Lean program. When placed in a `do` block, `idbg` captures all local variables in scope and expression `e`, then: - **In the language server**: starts a TCP server on localhost waiting for the running program to connect; the editor will mark this part of the program as "in progress" during this wait but that will not block `lake build` of the project. - **In the compiled program**: on first execution of the `idbg` call site, connects to the server, receives the expression, compiles and evaluates it using the program's actual runtime values, and sends the `repr` result back. The result is displayed as an info diagnostic on the `idbg` keyword. The expression `e` can be edited while the program is running - each edit triggers re-elaboration of `e`, a new TCP exchange, and an updated result. This makes `idbg` a live REPL for inspecting and experimenting with program state at a specific point in execution. Only when `idbg` is inserted, moved, or removed does the program need to be recompiled and restarted. # Known Limitations * The program will poll for the server for up to 10 minutes and needs to be killed manually otherwise. * Use of multiple `idbg` at once untested, likely too much overhead from overlapping imports without further changes. * `LEAN_PATH` must be properly set up so compiled program can import its origin module. * Untested on Windows and macOS.
This commit is contained in:
Sebastian Ullrich
GitHub
parent
ed0fd1e933
commit
8f80881c2f
6 changed files with 633 additions and 0 deletions
|
|
@ -66,3 +66,4 @@ public import Lean.Elab.DocString
|
|||
public import Lean.Elab.DocString.Builtin
|
||||
public import Lean.Elab.Parallel
|
||||
public import Lean.Elab.BuiltinDo
|
||||
public import Lean.Elab.Idbg
|
||||
|
|
|
|||
379
src/Lean/Elab/Idbg.lean
Normal file
379
src/Lean/Elab/Idbg.lean
Normal file
|
|
@ -0,0 +1,379 @@
|
|||
/-
|
||||
Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Sebastian Ullrich
|
||||
-/
|
||||
module
|
||||
|
||||
prelude
|
||||
public import Lean.Elab.Do.Basic
|
||||
meta import Lean.Parser.Do
|
||||
import Lean.Elab.Term
|
||||
import Lean.AddDecl
|
||||
import Lean.Environment
|
||||
import Lean.Data.Json
|
||||
import Lean.Compiler.IR.CompilerM
|
||||
import Init.System.IO
|
||||
public import Std.Internal.Async
|
||||
public import Std.Net.Addr
|
||||
|
||||
/-!
|
||||
# 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.
|
||||
-/
|
||||
|
||||
open Lean Lean.Elab Lean.Elab.Term Lean.Meta
|
||||
open Std.Net Std.Internal.IO.Async
|
||||
|
||||
namespace Lean.Idbg
|
||||
|
||||
/-- Custom `Name` serialization that preserves the exact structure.
|
||||
The standard `ToJson`/`FromJson Name` uses `toString`/`toName` which doesn't
|
||||
round-trip for hygienic names (e.g., names containing `@`). -/
|
||||
def nameToJson : Name → Json
|
||||
| .anonymous => Json.null
|
||||
| .str p s => Json.mkObj [("str", Json.arr #[nameToJson p, toJson s])]
|
||||
| .num p n => Json.mkObj [("num", Json.arr #[nameToJson p, n])]
|
||||
|
||||
/-- Inverse of `nameToJson`. -/
|
||||
partial def nameFromJson? (j : Json) : Except String Name := do
|
||||
if j.isNull then return .anonymous
|
||||
if let some arr := (j.getObjVal? "str").toOption then
|
||||
let #[p, s] := (← fromJson? arr : Array Json) | .error "str expects 2 elements"
|
||||
return .str (← nameFromJson? p) (← fromJson? s)
|
||||
if let some arr := (j.getObjVal? "num").toOption then
|
||||
let #[p, n] := (← fromJson? arr : Array Json) | .error "num expects 2 elements"
|
||||
return .num (← nameFromJson? p) (← fromJson? n)
|
||||
.error s!"expected Name, got {j}"
|
||||
|
||||
/-- Serialize `BinderInfo` to JSON. -/
|
||||
def binderInfoToJson : BinderInfo → Json
|
||||
| .default => "default"
|
||||
| .implicit => "implicit"
|
||||
| .strictImplicit => "strictImplicit"
|
||||
| .instImplicit => "instImplicit"
|
||||
|
||||
/-- Deserialize `BinderInfo` from JSON. -/
|
||||
def binderInfoFromJson? : Json → Except String BinderInfo
|
||||
| .str "default" => .ok .default
|
||||
| .str "implicit" => .ok .implicit
|
||||
| .str "strictImplicit" => .ok .strictImplicit
|
||||
| .str "instImplicit" => .ok .instImplicit
|
||||
| j => .error s!"expected BinderInfo, got {j}"
|
||||
|
||||
/-- Serialize `Literal` to JSON. -/
|
||||
def literalToJson : Literal → Json
|
||||
| .natVal n => Json.mkObj [("natVal", n)]
|
||||
| .strVal s => Json.mkObj [("strVal", s)]
|
||||
|
||||
/-- Deserialize `Literal` from JSON. -/
|
||||
def literalFromJson? (j : Json) : Except String Literal := do
|
||||
if let some n := (j.getObjVal? "natVal").toOption then
|
||||
return .natVal (← fromJson? n)
|
||||
if let some s := (j.getObjVal? "strVal").toOption then
|
||||
return .strVal (← fromJson? s)
|
||||
.error s!"expected Literal, got {j}"
|
||||
|
||||
/-- Serialize `Level` to JSON. -/
|
||||
partial def levelToJson : Level → Json
|
||||
| .zero => Json.mkObj [("zero", Json.null)]
|
||||
| .succ l => Json.mkObj [("succ", levelToJson l)]
|
||||
| .max a b => Json.mkObj [("max", Json.arr #[levelToJson a, levelToJson b])]
|
||||
| .imax a b => Json.mkObj [("imax", Json.arr #[levelToJson a, levelToJson b])]
|
||||
| .param n => Json.mkObj [("param", nameToJson n)]
|
||||
| .mvar id => Json.mkObj [("mvar", nameToJson id.name)]
|
||||
|
||||
/-- Deserialize `Level` from JSON. -/
|
||||
partial def levelFromJson? (j : Json) : Except String Level := do
|
||||
if (j.getObjVal? "zero").toOption.isSome then
|
||||
return .zero
|
||||
if let some l := (j.getObjVal? "succ").toOption then
|
||||
return .succ (← levelFromJson? l)
|
||||
if let some arr := (j.getObjVal? "max").toOption then
|
||||
let #[a, b] := (← fromJson? arr : Array Json) | .error "max expects 2 elements"
|
||||
return .max (← levelFromJson? a) (← levelFromJson? b)
|
||||
if let some arr := (j.getObjVal? "imax").toOption then
|
||||
let #[a, b] := (← fromJson? arr : Array Json) | .error "imax expects 2 elements"
|
||||
return .imax (← levelFromJson? a) (← levelFromJson? b)
|
||||
if let some n := (j.getObjVal? "param").toOption then
|
||||
return .param (← nameFromJson? n)
|
||||
if let some n := (j.getObjVal? "mvar").toOption then
|
||||
return .mvar ⟨← nameFromJson? n⟩
|
||||
.error s!"expected Level, got {j}"
|
||||
|
||||
/-- Serialize `Expr` to JSON. Metadata is stripped; free variables are preserved. -/
|
||||
partial def exprToJson : Expr → Json
|
||||
| .bvar i => Json.mkObj [("bvar", i)]
|
||||
| .fvar id => Json.mkObj [("fvar", nameToJson id.name)]
|
||||
| .mvar id => Json.mkObj [("mvar", nameToJson id.name)]
|
||||
| .sort l => Json.mkObj [("sort", levelToJson l)]
|
||||
| .const n ls => Json.mkObj [("const", nameToJson n), ("levels", Json.arr (ls.toArray.map levelToJson))]
|
||||
| .app fn arg => Json.mkObj [("app", Json.arr #[exprToJson fn, exprToJson arg])]
|
||||
| .lam n ty b bi => Json.mkObj [("lam", Json.mkObj [("name", nameToJson n), ("type", exprToJson ty), ("body", exprToJson b), ("bi", binderInfoToJson bi)])]
|
||||
| .forallE n ty b bi => Json.mkObj [("forallE", Json.mkObj [("name", nameToJson n), ("type", exprToJson ty), ("body", exprToJson b), ("bi", binderInfoToJson bi)])]
|
||||
| .letE n ty v b nd => Json.mkObj [("letE", Json.mkObj [("name", nameToJson n), ("type", exprToJson ty), ("value", exprToJson v), ("body", exprToJson b), ("nondep", nd)])]
|
||||
| .lit l => Json.mkObj [("lit", literalToJson l)]
|
||||
| .mdata _ e => exprToJson e -- strip metadata
|
||||
| .proj tn i s => Json.mkObj [("proj", Json.mkObj [("typeName", nameToJson tn), ("idx", i), ("struct", exprToJson s)])]
|
||||
|
||||
/-- Deserialize `Expr` from JSON. -/
|
||||
partial def exprFromJson? (j : Json) : Except String Expr := do
|
||||
if let some i := (j.getObjVal? "bvar").toOption then
|
||||
return .bvar (← fromJson? i)
|
||||
if let some id := (j.getObjVal? "fvar").toOption then
|
||||
return .fvar ⟨← nameFromJson? id⟩
|
||||
if let some id := (j.getObjVal? "mvar").toOption then
|
||||
return .mvar ⟨← nameFromJson? id⟩
|
||||
if let some l := (j.getObjVal? "sort").toOption then
|
||||
return .sort (← levelFromJson? l)
|
||||
if (j.getObjVal? "const").toOption.isSome then
|
||||
let n ← nameFromJson? (← j.getObjVal? "const")
|
||||
let ls : Array Json ← fromJson? (← j.getObjVal? "levels")
|
||||
return .const n (← ls.toList.mapM levelFromJson?)
|
||||
if let some arr := (j.getObjVal? "app").toOption then
|
||||
let #[fn, arg] := (← fromJson? arr : Array Json) | .error "app expects 2 elements"
|
||||
return .app (← exprFromJson? fn) (← exprFromJson? arg)
|
||||
if let some obj := (j.getObjVal? "lam").toOption then
|
||||
return .lam (← nameFromJson? (← obj.getObjVal? "name"))
|
||||
(← exprFromJson? (← obj.getObjVal? "type"))
|
||||
(← exprFromJson? (← obj.getObjVal? "body"))
|
||||
(← binderInfoFromJson? (← obj.getObjVal? "bi"))
|
||||
if let some obj := (j.getObjVal? "forallE").toOption then
|
||||
return .forallE (← nameFromJson? (← obj.getObjVal? "name"))
|
||||
(← exprFromJson? (← obj.getObjVal? "type"))
|
||||
(← exprFromJson? (← obj.getObjVal? "body"))
|
||||
(← binderInfoFromJson? (← obj.getObjVal? "bi"))
|
||||
if let some obj := (j.getObjVal? "letE").toOption then
|
||||
return .letE (← nameFromJson? (← obj.getObjVal? "name"))
|
||||
(← exprFromJson? (← obj.getObjVal? "type"))
|
||||
(← exprFromJson? (← obj.getObjVal? "value"))
|
||||
(← exprFromJson? (← obj.getObjVal? "body"))
|
||||
(← fromJson? (← obj.getObjVal? "nondep"))
|
||||
if let some l := (j.getObjVal? "lit").toOption then
|
||||
return .lit (← literalFromJson? l)
|
||||
if let some obj := (j.getObjVal? "proj").toOption then
|
||||
return .proj (← nameFromJson? (← obj.getObjVal? "typeName"))
|
||||
(← fromJson? (← obj.getObjVal? "idx"))
|
||||
(← exprFromJson? (← obj.getObjVal? "struct"))
|
||||
.error s!"expected Expr, got {j}"
|
||||
|
||||
/-- Deterministic port for a given `idbg` site, in range [10000, 65535]. -/
|
||||
def idbgPort (siteId : String) : UInt16 :=
|
||||
let h := hash siteId
|
||||
(h % 55535 + 10000).toUInt16
|
||||
|
||||
def sendMsg (client : TCP.Socket.Client) (msg : String) : IO Unit := do
|
||||
let bytes := msg.toUTF8
|
||||
let header := s!"{bytes.size}\n".toUTF8
|
||||
let t ← (client.sendAll #[header, bytes]).toIO
|
||||
t.block
|
||||
|
||||
def recvMsg (client : TCP.Socket.Client) : IO String := do
|
||||
-- Read until newline to get the decimal length
|
||||
let mut header := ByteArray.empty
|
||||
repeat
|
||||
let t ← (client.recv? 1).toIO
|
||||
let some chunk ← t.block | throw (.userError "idbg: connection closed")
|
||||
if chunk[0]! == '\n'.toUInt8 then break
|
||||
header := header ++ chunk
|
||||
let some lenStr := String.fromUTF8? header | throw (.userError "idbg: invalid header")
|
||||
let some len := lenStr.toNat? | throw (.userError "idbg: invalid length")
|
||||
let mut payload := ByteArray.empty
|
||||
while payload.size < len do
|
||||
let t ← (client.recv? (len - payload.size).toUInt64).toIO
|
||||
let some chunk ← t.block | throw (.userError "idbg: connection closed")
|
||||
payload := payload ++ chunk
|
||||
let some s := String.fromUTF8? payload | throw (.userError "idbg: invalid UTF-8")
|
||||
return s
|
||||
|
||||
/-- Start a TCP server on the deterministic port for this site,
|
||||
wait for one connection, send expression JSON, and receive the result string.
|
||||
Returns `none` if the port is still held by a previous (cancelled) server. -/
|
||||
def idbgServer (siteId : String) (exprJson : Json) : IO (Option String) := do
|
||||
let port := idbgPort siteId
|
||||
let addr := SocketAddressV4.mk (.ofParts 127 0 0 1) port
|
||||
let mut server? : Option TCP.Socket.Server := none
|
||||
for _ in List.range 100 do -- retry for up to 10s
|
||||
match (← (do let s ← TCP.Socket.Server.mk; s.bind addr; s.listen 1; return s).toBaseIO) with
|
||||
| .ok s => server? := some s; break
|
||||
| .error _ => IO.sleep 100
|
||||
let some server := server? | return none
|
||||
let t ← server.accept |>.toIO
|
||||
let client ← t.block
|
||||
sendMsg client exprJson.compress
|
||||
let result ← recvMsg client
|
||||
let t ← client.shutdown |>.toIO
|
||||
t.block
|
||||
return some result
|
||||
|
||||
/-- Load the program's environment from its imports.
|
||||
The imports include the current module (appended last by the elaborator) so that
|
||||
same-file declarations are available. If its `.olean` is not found (e.g., when
|
||||
running `lean` directly), we fall back to just the transitive imports. -/
|
||||
def idbgLoadEnv (imports : Array Import) : IO Environment := do
|
||||
try
|
||||
importModules imports {} 0
|
||||
catch _ =>
|
||||
importModules imports.pop {} 0
|
||||
|
||||
/-- Compile and evaluate an expression in the given environment. -/
|
||||
def idbgCompileAndEval (α : Type) [Nonempty α]
|
||||
(env : Environment) (type value : Expr) : IO α := do
|
||||
let name := `_idbg
|
||||
let decl := Declaration.defnDecl {
|
||||
name
|
||||
levelParams := []
|
||||
type
|
||||
value
|
||||
hints := .opaque
|
||||
safety := .unsafe
|
||||
}
|
||||
let ((), {env := env', ..}) ← (addAndCompile decl).toIO
|
||||
{ fileName := "<idbg>", fileMap := default, options := {} }
|
||||
{ env }
|
||||
match unsafe env'.evalConst α {} name (checkMeta := false) with
|
||||
| .ok val => return val
|
||||
| .error msg => throw (.userError s!"idbg evalConst failed: {msg}")
|
||||
|
||||
/-- Connect to the debug server, receive expressions, evaluate, send results. Loops forever. -/
|
||||
public def idbgClientLoop {α : Type} [Nonempty α]
|
||||
(siteId : String) (imports : Array Import) (apply : α → String) : IO Unit := do
|
||||
let baseEnv ← idbgLoadEnv imports
|
||||
let port := idbgPort siteId
|
||||
let addr := SocketAddressV4.mk (.ofParts 127 0 0 1) port
|
||||
while true do
|
||||
try
|
||||
let client ← TCP.Socket.Client.mk
|
||||
let t ← (client.connect addr).toIO
|
||||
t.block
|
||||
let msg ← recvMsg client
|
||||
let json ← IO.ofExcept (Json.parse msg)
|
||||
let type ← IO.ofExcept (exprFromJson? (← IO.ofExcept (json.getObjVal? "type")))
|
||||
let value ← IO.ofExcept (exprFromJson? (← IO.ofExcept (json.getObjVal? "value")))
|
||||
let fnVal ← idbgCompileAndEval α baseEnv type value
|
||||
let result := apply fnVal
|
||||
sendMsg client result
|
||||
let t ← client.shutdown |>.toIO
|
||||
t.block
|
||||
catch e =>
|
||||
-- Only log non-connection errors (connection refused is normal during reconnect)
|
||||
let msg := toString e
|
||||
unless (msg.find? "connection refused").isSome do
|
||||
IO.eprintln s!"idbg client: {e}"
|
||||
IO.sleep 500
|
||||
|
||||
end Lean.Idbg
|
||||
|
||||
namespace Lean.Elab.Do
|
||||
|
||||
open Lean.Idbg
|
||||
|
||||
@[builtin_doElem_control_info Lean.Parser.Term.doIdbg]
|
||||
def controlInfoIdbg : ControlInfoHandler := fun _ => return default
|
||||
|
||||
/-- Core elaboration logic shared by term and do-element forms.
|
||||
Elaborates `e`, wraps the result in `toString ∘ repr`, abstracts over all local declarations,
|
||||
and generates both the server-side TCP exchange and the runtime client loop code. -/
|
||||
private def elabIdbgCore (e : Syntax) (body : TSyntax `term) (ref : Syntax) (expectedType? : Option Expr) :
|
||||
TermElabM Expr := do
|
||||
let fileName ← IO.FS.realPath (← getFileName)
|
||||
let siteId := toString (hash s!"{fileName}:{ref.getPos?.getD 0}")
|
||||
|
||||
-- Collect ALL non-aux local declarations.
|
||||
-- We need all of them (not just those used in the current expression)
|
||||
-- because the expression can change on the server side while the
|
||||
-- compiled program's apply closure is fixed.
|
||||
let lctx ← getLCtx
|
||||
let mut localDecls : Array LocalDecl := #[]
|
||||
for decl in lctx do
|
||||
if decl.isAuxDecl then continue
|
||||
localDecls := localDecls.push decl
|
||||
let localFVars := localDecls.map (mkFVar ·.fvarId)
|
||||
|
||||
-- Elaborate e, wrap in `toString ∘ repr`.
|
||||
-- `synthesizeSyntheticMVarsNoPostponing` forces pending instance resolution
|
||||
-- so that `instantiateMVars` can fully resolve all metavariables.
|
||||
let eExpr ← Term.elabTerm e none
|
||||
Term.synthesizeSyntheticMVarsNoPostponing
|
||||
let eExpr ← instantiateMVars eExpr
|
||||
let reprExpr ← Meta.mkAppM ``repr #[eExpr]
|
||||
let reprStrExpr ← Meta.mkAppM ``toString #[reprExpr]
|
||||
Term.synthesizeSyntheticMVarsNoPostponing
|
||||
let reprStrExpr ← instantiateMVars reprStrExpr
|
||||
|
||||
-- Abstract over ALL locals as lambdas (not lets).
|
||||
-- Do-notation let-bindings have `nondep := false`, so `mkLambdaFVars` would
|
||||
-- create `letE` for them. We temporarily set `nondep := true` so that
|
||||
-- `generalizeNondepLet` (the default) turns them all into lambdas.
|
||||
let lctx' := localDecls.foldl (init := ← getLCtx) fun lctx decl =>
|
||||
lctx.modifyLocalDecl decl.fvarId (·.setNondep true)
|
||||
let (abstractedValue, abstractedType) ← withLCtx' lctx' do
|
||||
let abstractedValue ← Meta.mkLambdaFVars localFVars reprStrExpr
|
||||
let abstractedType ← Meta.inferType abstractedValue
|
||||
return (← instantiateMVars abstractedValue, ← instantiateMVars abstractedType)
|
||||
|
||||
if abstractedValue.hasMVar then
|
||||
throwError "idbg: abstracted value still has metavariables"
|
||||
if abstractedType.hasMVar then
|
||||
throwError "idbg: abstracted type still has metavariables"
|
||||
|
||||
-- Server mode: serialize and serve in a background snapshot task.
|
||||
-- Skip if expression contains sorry (partial input during editing).
|
||||
if Elab.inServer.get (← getOptions) && !abstractedValue.hasSorry then
|
||||
let json := Json.mkObj [
|
||||
("type", exprToJson abstractedType),
|
||||
("value", exprToJson abstractedValue)
|
||||
]
|
||||
let cancelTk ← IO.CancelToken.new
|
||||
let act ← Core.wrapAsyncAsSnapshot (cancelTk? := cancelTk) fun () => do
|
||||
if let some result ← idbgServer siteId json then
|
||||
logInfoAt ref m!"idbg: {result}"
|
||||
Core.logSnapshotTask {
|
||||
stx? := some ref
|
||||
task := (← BaseIO.asTask (act ()))
|
||||
cancelTk? := cancelTk
|
||||
}
|
||||
|
||||
-- Generate runtime code: `idbgClientLoop siteId imports apply >>= fun _ => body`
|
||||
let siteLit := Syntax.mkStrLit siteId
|
||||
let applyClosure ← withLocalDecl `f .default abstractedType fun fVar => do
|
||||
let appBody := mkAppN fVar localFVars
|
||||
Meta.mkLambdaFVars #[fVar] appBody
|
||||
let closureStx ← Term.exprToSyntax applyClosure
|
||||
-- Include the current module so the client can access same-file declarations.
|
||||
-- The `.olean` should exist since the program was compiled from it.
|
||||
let imports := (← getEnv).header.imports.push { module := (← getEnv).mainModule }
|
||||
let importExprs ← imports.mapM fun imp => do
|
||||
let nameExpr := toExpr imp.module
|
||||
let importAllExpr := toExpr imp.importAll
|
||||
let isExportedExpr := toExpr imp.isExported
|
||||
let isMetaExpr := toExpr imp.isMeta
|
||||
return mkAppN (.const ``Import.mk []) #[nameExpr, importAllExpr, isExportedExpr, isMetaExpr]
|
||||
let importsExpr := mkApp2 (.const ``List.toArray [.zero])
|
||||
(.const ``Import [])
|
||||
(importExprs.toList.foldr (fun e acc => mkApp3 (.const ``List.cons [.zero]) (.const ``Import []) e acc)
|
||||
(mkApp (.const ``List.nil [.zero]) (.const ``Import [])))
|
||||
let importsStx ← Term.exprToSyntax importsExpr
|
||||
Term.elabTerm (← `(
|
||||
Lean.Idbg.idbgClientLoop $siteLit $importsStx $closureStx >>= fun _ => $body
|
||||
)) expectedType?
|
||||
|
||||
@[builtin_term_elab Lean.Parser.Term.idbg]
|
||||
def elabIdbgTerm : TermElab := fun stx expectedType? => do
|
||||
let `(Lean.Parser.Term.idbg| idbg $e; $body) := stx | throwUnsupportedSyntax
|
||||
elabIdbgCore (e := e) (body := body) (ref := stx) expectedType?
|
||||
|
||||
@[builtin_doElem_elab Lean.Parser.Term.doIdbg]
|
||||
def elabDoIdbg : DoElab := fun stx dec => do
|
||||
let `(Lean.Parser.Term.doIdbg| idbg $e) := stx | throwUnsupportedSyntax
|
||||
let mγ ← mkMonadicType (← read).doBlockResultType
|
||||
doElabToSyntax "idbg body" dec.continueWithUnit fun body => do
|
||||
elabIdbgCore (e := e) (body := body) (ref := stx) mγ
|
||||
|
||||
end Lean.Elab.Do
|
||||
|
|
@ -224,6 +224,36 @@ It should only be used for debugging.
|
|||
@[builtin_doElem_parser] def doDbgTrace := leading_parser:leadPrec
|
||||
"dbg_trace " >> ((interpolatedStr termParser) <|> termParser)
|
||||
/--
|
||||
*experimental*
|
||||
|
||||
`idbg e` enables live inspection of program state from the editor. When placed in a `do` block,
|
||||
it captures all local variables in scope and the expression `e`, then:
|
||||
|
||||
- **In the language server**: starts a TCP server on localhost waiting for the running program to
|
||||
connect; the editor will mark this part of the program as "in progress" during this wait but that
|
||||
will not block `lake build` of the project.
|
||||
- **In the compiled program**: on first execution of the `idbg` call site, connects to the server,
|
||||
receives the expression, compiles and evaluates it using the program's actual runtime values, and
|
||||
sends the `repr` result back.
|
||||
|
||||
The result is displayed as an info diagnostic on the `idbg` keyword. The expression `e` can be
|
||||
edited while the program is running - each edit triggers re-elaboration of `e`, a new TCP exchange,
|
||||
and an updated result. This makes `idbg` a live REPL for inspecting and experimenting with
|
||||
program state at a specific point in execution. Only when `idbg` is inserted, moved, or removed does
|
||||
the program need to be recompiled and restarted.
|
||||
|
||||
# Known Limitations
|
||||
|
||||
* The program will poll for the server for up to 10 minutes and needs to be killed manually
|
||||
otherwise.
|
||||
* Use of multiple `idbg` at once untested, likely too much overhead from overlapping imports without
|
||||
further changes.
|
||||
* `LEAN_PATH` must be properly set up so compiled program can import its origin module.
|
||||
* Untested on Windows and macOS.
|
||||
-/
|
||||
@[builtin_doElem_parser] def doIdbg := leading_parser:leadPrec
|
||||
withPosition ("idbg " >> termParser)
|
||||
/--
|
||||
`assert! cond` panics if `cond` evaluates to `false`.
|
||||
-/
|
||||
@[builtin_doElem_parser] def doAssert := leading_parser:leadPrec
|
||||
|
|
|
|||
|
|
@ -912,6 +912,10 @@ interpolated string literal) to stderr. It should only be used for debugging.
|
|||
@[builtin_term_parser] def dbgTrace := leading_parser:leadPrec
|
||||
withPosition ("dbg_trace" >> (interpolatedStr termParser <|> termParser)) >>
|
||||
optSemicolon termParser
|
||||
/-- Term-level form of the interactive debugger. See the `doIdbg` do element for full documentation. -/
|
||||
@[builtin_term_parser] def «idbg» := leading_parser:leadPrec
|
||||
withPosition ("idbg " >> checkColGt >> termParser) >>
|
||||
optSemicolon termParser
|
||||
/-- `assert! cond` panics if `cond` evaluates to `false`. -/
|
||||
@[builtin_term_parser] def assert := leading_parser:leadPrec
|
||||
withPosition ("assert! " >> termParser) >> optSemicolon termParser
|
||||
|
|
|
|||
13
tests/lean/run/idbg_basic.lean
Normal file
13
tests/lean/run/idbg_basic.lean
Normal file
|
|
@ -0,0 +1,13 @@
|
|||
module
|
||||
|
||||
import Lean
|
||||
|
||||
/-! ## idbg syntax compiles in a do block -/
|
||||
|
||||
-- Verify the idbg syntax is accepted and type-checks.
|
||||
-- We can't run this (the client loop would try to connect), just check elaboration.
|
||||
-- Disable inServer so the elaborator doesn't block waiting for TCP connection
|
||||
set_option Elab.inServer false in
|
||||
set_option backward.do.legacy false in
|
||||
def idbgTypeCheck (x : Nat) (s : String) : IO Unit := do
|
||||
idbg x + s.length
|
||||
206
tests/lean/run/idbg_e2e.lean
Normal file
206
tests/lean/run/idbg_e2e.lean
Normal file
|
|
@ -0,0 +1,206 @@
|
|||
module
|
||||
|
||||
import Lean
|
||||
import all Lean.Elab.Idbg
|
||||
import Std.Internal.Async
|
||||
import Std.Net.Addr
|
||||
|
||||
/-! ## Part 1: Expr JSON round-trip with hygienic names -/
|
||||
|
||||
open Lean Lean.Idbg Std.Net Std.Internal.IO.Async in
|
||||
#eval show IO Unit from do
|
||||
-- `_@` contains `@` which breaks the standard Name.toString/toName round-trip
|
||||
let hygName := Name.mkNum (.mkStr (.mkNum (.mkStr (.mkStr .anonymous "_@") "test") 42) "_hyg") 6
|
||||
|
||||
-- Lambda with hygienic name
|
||||
let e := Expr.lam hygName (.const ``Nat []) (.bvar 0) .default
|
||||
let j := exprToJson e
|
||||
let d ← IO.ofExcept (exprFromJson? j)
|
||||
let Expr.lam n .. := d | throw (IO.userError "expected lam")
|
||||
assert! n == hygName
|
||||
|
||||
-- Const with universe levels
|
||||
let e2 := Expr.const ``List [.param `u]
|
||||
let j2 := exprToJson e2
|
||||
let d2 ← IO.ofExcept (exprFromJson? j2)
|
||||
let Expr.const n2 ls2 := d2 | throw (IO.userError "expected const")
|
||||
assert! n2 == ``List
|
||||
assert! ls2 == [.param `u]
|
||||
|
||||
/-! ## Part 2: Manual TCP server/client round-trip with hand-built expression -/
|
||||
|
||||
open Lean Lean.Idbg Std.Net Std.Internal.IO.Async in
|
||||
#eval show IO Unit from do
|
||||
let siteId := "test-e2e"
|
||||
let env ← importModules #[{ module := `Init }] {} 0
|
||||
|
||||
-- Build: fun (x : Nat) => toString (Nat.add x 1)
|
||||
let value := Expr.lam `x (.const ``Nat []) (mkApp3 (.const ``ToString.toString [.zero])
|
||||
(.const ``Nat [])
|
||||
(.const ``instToStringNat [])
|
||||
(mkApp2 (.const ``Nat.add []) (.bvar 0) (mkNatLit 1))) .default
|
||||
let type := Expr.forallE `x (.const ``Nat []) (.const ``String []) .default
|
||||
|
||||
let exprJson := Json.mkObj [
|
||||
("type", exprToJson type),
|
||||
("value", exprToJson value)
|
||||
]
|
||||
|
||||
-- Run server in background
|
||||
let serverTask ← IO.asTask (idbgServer siteId exprJson)
|
||||
|
||||
-- Give server time to bind
|
||||
IO.sleep 100
|
||||
|
||||
-- Connect to deterministic port
|
||||
let port := idbgPort siteId
|
||||
let client ← TCP.Socket.Client.mk
|
||||
let addr := SocketAddressV4.mk (.ofParts 127 0 0 1) port
|
||||
let t ← (client.connect addr).toIO
|
||||
t.block
|
||||
|
||||
-- Receive length-prefixed message (decimal length + newline + payload)
|
||||
let mut hdr := ByteArray.empty
|
||||
repeat
|
||||
let t ← (client.recv? 1).toIO
|
||||
let some chunk ← t.block | throw (IO.userError "connection closed")
|
||||
if chunk[0]! == '\n'.toUInt8 then break
|
||||
hdr := hdr ++ chunk
|
||||
let some hdrStr := String.fromUTF8? hdr | throw (IO.userError "invalid header")
|
||||
let some len := hdrStr.toNat? | throw (IO.userError "invalid length")
|
||||
let mut payload := ByteArray.empty
|
||||
while payload.size < len do
|
||||
let t ← (client.recv? (len - payload.size).toUInt64).toIO
|
||||
let some chunk ← t.block | throw (IO.userError "connection closed")
|
||||
payload := payload ++ chunk
|
||||
let some msg := String.fromUTF8? payload | throw (IO.userError "invalid UTF-8")
|
||||
|
||||
-- Parse and compile
|
||||
let json ← IO.ofExcept (Json.parse msg)
|
||||
let recvType ← IO.ofExcept (exprFromJson? (← IO.ofExcept (json.getObjVal? "type")))
|
||||
let recvValue ← IO.ofExcept (exprFromJson? (← IO.ofExcept (json.getObjVal? "value")))
|
||||
|
||||
let declName := `_idbg_test
|
||||
let decl := Declaration.defnDecl {
|
||||
name := declName
|
||||
levelParams := []
|
||||
type := recvType
|
||||
value := recvValue
|
||||
hints := .opaque
|
||||
safety := .unsafe
|
||||
}
|
||||
let ((), {env := env', ..}) ← (addAndCompile decl).toIO
|
||||
{ fileName := "<idbg-test>", fileMap := default, options := {} }
|
||||
{ env }
|
||||
let result := match env'.evalConst (Nat → String) {} declName (checkMeta := false) with
|
||||
| .ok f => f 41 -- 41 + 1 = 42
|
||||
| .error msg => s!"evalConst failed: {msg}"
|
||||
|
||||
-- Send result back (length-prefixed)
|
||||
let resultBytes := result.toUTF8
|
||||
let resultHdr := s!"{resultBytes.size}\n".toUTF8
|
||||
let t ← (client.sendAll #[resultHdr, resultBytes]).toIO
|
||||
t.block
|
||||
let t ← client.shutdown |>.toIO
|
||||
t.block
|
||||
|
||||
-- Verify server received "42"
|
||||
let serverResult ← IO.ofExcept (← IO.wait serverTask)
|
||||
assert! serverResult == some "42"
|
||||
|
||||
/-! ## Part 3: Full pipeline through the real elaborator
|
||||
|
||||
Run `lean -DElab.inServer=true` on a file containing `idbg`, then act as the
|
||||
client: receive the expression JSON, compile it, evaluate it, send result back.
|
||||
This is the actual end-to-end flow that happens between the editor and a running program.
|
||||
We do this TWICE to test reconnection (simulating the user editing the expression). -/
|
||||
|
||||
open Lean Lean.Idbg Std.Net Std.Internal.IO.Async in
|
||||
#eval show IO Unit from do
|
||||
let lean := (← IO.appDir) / "lean"
|
||||
let env ← importModules #[{ module := `Init }] {} 0
|
||||
|
||||
-- Helper: run lean on a test file with idbg, act as client, compile the received expression
|
||||
let doExchange := fun (env : Environment) (testCode : String) (idbgPos : Nat) => do
|
||||
let testFile : System.FilePath := "/tmp" / "idbg_e2e_test.lean"
|
||||
IO.FS.writeFile testFile testCode
|
||||
let realPath ← IO.FS.realPath testFile
|
||||
let siteId := toString (hash s!"{realPath}:{idbgPos}")
|
||||
let port := idbgPort siteId
|
||||
|
||||
let child ← IO.Process.spawn {
|
||||
cmd := lean.toString
|
||||
args := #["-DElab.inServer=true", testFile.toString]
|
||||
stdout := .piped
|
||||
stderr := .piped
|
||||
}
|
||||
|
||||
-- Retry connecting until the server binds
|
||||
let addr := SocketAddressV4.mk (.ofParts 127 0 0 1) port
|
||||
let mut client ← TCP.Socket.Client.mk
|
||||
let mut connected := false
|
||||
for _ in List.range 200 do
|
||||
match (← (do let t ← (client.connect addr).toIO; t.block : IO Unit).toBaseIO) with
|
||||
| .ok () => connected := true; break
|
||||
| .error _ => IO.sleep 100; client ← TCP.Socket.Client.mk
|
||||
unless connected do
|
||||
let stderr ← child.stderr.readToEnd
|
||||
throw (IO.userError s!"Could not connect to port {port}. stderr: {stderr}")
|
||||
|
||||
-- Receive expression JSON (length-prefixed: decimal length + newline + payload)
|
||||
let mut hdr := ByteArray.empty
|
||||
repeat
|
||||
let t ← (client.recv? 1).toIO
|
||||
let some chunk ← t.block | throw (IO.userError "connection closed")
|
||||
if chunk[0]! == '\n'.toUInt8 then break
|
||||
hdr := hdr ++ chunk
|
||||
let some hdrStr := String.fromUTF8? hdr | throw (IO.userError "invalid header")
|
||||
let some len := hdrStr.toNat? | throw (IO.userError "invalid length")
|
||||
let mut payload := ByteArray.empty
|
||||
while payload.size < len do
|
||||
let t ← (client.recv? (len - payload.size).toUInt64).toIO
|
||||
let some chunk ← t.block | throw (IO.userError "connection closed")
|
||||
payload := payload ++ chunk
|
||||
let some msg := String.fromUTF8? payload | throw (IO.userError "invalid UTF-8")
|
||||
|
||||
let json ← IO.ofExcept (Json.parse msg)
|
||||
let recvType ← IO.ofExcept (exprFromJson? (← IO.ofExcept (json.getObjVal? "type")))
|
||||
let recvValue ← IO.ofExcept (exprFromJson? (← IO.ofExcept (json.getObjVal? "value")))
|
||||
|
||||
-- Verify no metavariables
|
||||
if recvValue.hasMVar then throw (IO.userError "Expression value has metavariables!")
|
||||
if recvType.hasMVar then throw (IO.userError "Expression type has metavariables!")
|
||||
|
||||
-- Compile (this is where "declaration has metavariables" would fail)
|
||||
let declName := .mkNum `_idbg_e2e_real (← IO.rand 0 1000000)
|
||||
let decl := Declaration.defnDecl {
|
||||
name := declName
|
||||
levelParams := []
|
||||
type := recvType
|
||||
value := recvValue
|
||||
hints := .opaque
|
||||
safety := .unsafe
|
||||
}
|
||||
let ((), {env := env', ..}) ← (addAndCompile decl).toIO
|
||||
{ fileName := "<idbg-test>", fileMap := default, options := {} }
|
||||
{ env }
|
||||
|
||||
-- Send dummy result back (length-prefixed)
|
||||
let resultBytes := "test-ok".toUTF8
|
||||
let resultHdr := s!"{resultBytes.size}\n".toUTF8
|
||||
let t ← (client.sendAll #[resultHdr, resultBytes]).toIO
|
||||
t.block
|
||||
let t ← client.shutdown |>.toIO
|
||||
t.block
|
||||
let _ ← child.wait
|
||||
return env'
|
||||
|
||||
-- Exchange 1: `idbg x + s.length`
|
||||
-- idbg at byte 108 in this string
|
||||
let code1 := "import Lean\nset_option backward.do.legacy false\ndef main : IO Unit := do\n let x := 42\n let s := \"hello\"\n idbg x + s.length\n"
|
||||
let env' ← doExchange env code1 108
|
||||
|
||||
-- Exchange 2: `idbg x + s.length + 1` (the expression that triggered the mvar bug)
|
||||
-- idbg at byte 108 in this string too
|
||||
let code2 := "import Lean\nset_option backward.do.legacy false\ndef main : IO Unit := do\n let x := 42\n let s := \"hello\"\n idbg x + s.length + 1\n"
|
||||
let _ ← doExchange env' code2 108
|
||||
Loading…
Add table
Reference in a new issue