From 10668344924be48b42a6774d029a6cfa5271ed30 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 24 Feb 2026 21:35:37 +0100 Subject: [PATCH 1/9] Rebrand project to ImpLab and reorganize debugger modules Drop stale ProgramInfoLoader import after rebase --- .vscode/launch.json | 6 +- .vscode/tasks.json | 4 +- AGENTS.md | 14 +-- DAP_PLAN.md | 2 +- Dap.lean | 21 ---- ImpLab.lean | 21 ++++ {Dap => ImpLab}/Debugger/Core.lean | 6 +- .../Debugger}/DAP/Capabilities.lean | 4 +- {Dap => ImpLab/Debugger}/DAP/Export.lean | 26 ++--- {Dap => ImpLab/Debugger}/DAP/Launch.lean | 6 +- {Dap => ImpLab/Debugger}/DAP/Resolve.lean | 10 +- {Dap => ImpLab/Debugger}/DAP/Stdio.lean | 40 ++++---- {Dap => ImpLab}/Debugger/Session.lean | 8 +- {Dap => ImpLab/Debugger}/Widget/Server.lean | 26 ++--- {Dap => ImpLab/Debugger}/Widget/Types.lean | 6 +- {Dap => ImpLab/Debugger}/Widget/UI.lean | 16 +-- {Dap => ImpLab}/Lang/Ast.lean | 4 +- {Dap => ImpLab}/Lang/Dsl.lean | 6 +- {Dap => ImpLab}/Lang/Eval.lean | 6 +- {Dap => ImpLab}/Lang/History.lean | 4 +- {Dap => ImpLab}/Lang/Trace.lean | 8 +- README.md | 70 ++++++------- Test/Core.lean | 98 +++++++++---------- Test/Main.lean | 4 +- Test/Transport.lean | 10 +- Test/Util.lean | 6 +- app/ExportMain.lean | 4 +- app/ToyDap.lean | 4 +- client/README.md | 8 +- client/package.json | 18 ++-- client/src/extension.ts | 8 +- examples/Main.lean | 14 +-- dap.code-workspace => implab.code-workspace | 0 lakefile.toml | 4 +- 34 files changed, 246 insertions(+), 246 deletions(-) delete mode 100644 Dap.lean create mode 100644 ImpLab.lean rename {Dap => ImpLab}/Debugger/Core.lean (99%) rename {Dap => ImpLab/Debugger}/DAP/Capabilities.lean (93%) rename {Dap => ImpLab/Debugger}/DAP/Export.lean (82%) rename {Dap => ImpLab/Debugger}/DAP/Launch.lean (89%) rename {Dap => ImpLab/Debugger}/DAP/Resolve.lean (91%) rename {Dap => ImpLab/Debugger}/DAP/Stdio.lean (93%) rename {Dap => ImpLab}/Debugger/Session.lean (99%) rename {Dap => ImpLab/Debugger}/Widget/Server.lean (71%) rename {Dap => ImpLab/Debugger}/Widget/Types.lean (98%) rename {Dap => ImpLab/Debugger}/Widget/UI.lean (92%) rename {Dap => ImpLab}/Lang/Ast.lean (99%) rename {Dap => ImpLab}/Lang/Dsl.lean (99%) rename {Dap => ImpLab}/Lang/Eval.lean (99%) rename {Dap => ImpLab}/Lang/History.lean (95%) rename {Dap => ImpLab}/Lang/Trace.lean (96%) rename dap.code-workspace => implab.code-workspace (100%) diff --git a/.vscode/launch.json b/.vscode/launch.json index 1ad0431..bec1dac 100644 --- a/.vscode/launch.json +++ b/.vscode/launch.json @@ -2,15 +2,15 @@ "version": "0.2.0", "configurations": [ { - "name": "Toy DAP (auto-export ProgramInfo)", + "name": "ImpLab Toy DAP (auto-export ProgramInfo)", "type": "lean-toy-dap", "request": "launch", "source": "${workspaceFolder}/examples/Main.lean", "stopOnEntry": true, - "preLaunchTask": "Generate Toy DAP ProgramInfo" + "preLaunchTask": "Generate ImpLab ProgramInfo" }, { - "name": "Toy DAP (sample ProgramInfo fallback)", + "name": "ImpLab Toy DAP (sample ProgramInfo fallback)", "type": "lean-toy-dap", "request": "launch", "source": "${file}", diff --git a/.vscode/tasks.json b/.vscode/tasks.json index 935c4ca..66fdfa5 100644 --- a/.vscode/tasks.json +++ b/.vscode/tasks.json @@ -2,14 +2,14 @@ "version": "2.0.0", "tasks": [ { - "label": "Generate Toy DAP ProgramInfo", + "label": "Generate ImpLab ProgramInfo", "type": "process", "command": "lake", "args": [ "exe", "dap-export", "--decl", - "Dap.Lang.Examples.mainProgram", + "ImpLab.Lang.Examples.mainProgram", "--out", ".dap/programInfo.generated.json" ], diff --git a/AGENTS.md b/AGENTS.md index 9337214..87c416f 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -6,11 +6,11 @@ - Avoid compatibility shims during refactors; prefer direct clean structure. ## Main surfaces -- Runtime: `Dap/Lang/*.lean` -- Debugger source of truth: `Dap/Debugger/Core.lean` -- Session semantics: `Dap/Debugger/Session.lean` -- Lean RPC transport: `Dap/Widget/Server.lean` -- StdIO DAP transport: `Dap/DAP/Stdio.lean` + `app/ToyDap.lean` +- Runtime: `ImpLab/Lang/*.lean` +- Debugger source of truth: `ImpLab/Debugger/Core.lean` +- Session semantics: `ImpLab/Debugger/Session.lean` +- Lean RPC transport: `ImpLab/Debugger/Widget/Server.lean` +- StdIO DAP transport: `ImpLab/Debugger/DAP/Stdio.lean` + `app/ToyDap.lean` - VS Code client: `client/` ## Build/test commands @@ -21,7 +21,7 @@ - `cd client && npm run compile` ## Architecture guardrails -- Put new debugger behavior in `Dap/Debugger/Core.lean` first, then wire transports. +- Put new debugger behavior in `ImpLab/Debugger/Core.lean` first, then wire transports. - Keep transport files as adapters only; avoid protocol/state duplication. - Treat `ProgramInfo` as canonical across launch/debug/export flows. - `Program` remains function-only (`functions : Array FuncDef`) with required `main`. @@ -35,7 +35,7 @@ - Preserve stable DAP JSON payload shapes. ## Testing split -- Core behavior tests: `Dap/Debugger/Core.lean` APIs. +- Core behavior tests: `ImpLab/Debugger/Core.lean` APIs. - Transport tests: framing/serialization + request-to-core wiring. - DAP sanity tests: lifecycle ordering + at least one breakpoint hit path. diff --git a/DAP_PLAN.md b/DAP_PLAN.md index 1299a79..bf9d386 100644 --- a/DAP_PLAN.md +++ b/DAP_PLAN.md @@ -4,7 +4,7 @@ Canonical project guardrails, architecture rules, and validation commands live i This file is only for current DAP-facing priorities and open work. ## Active priorities -1. Remove any remaining duplicated behavior between `Dap/Widget/Server.lean` and `Dap/DAP/Stdio.lean` by lifting semantics to `Dap/Debugger/Core.lean`. +1. Remove any remaining duplicated behavior between `ImpLab/Debugger/Widget/Server.lean` and `ImpLab/Debugger/DAP/Stdio.lean` by lifting semantics to `ImpLab/Debugger/Core.lean`. 2. Keep line/function source mapping explicit and centralized so stack/breakpoint rendering stays consistent. 3. Preserve strict DAP lifecycle ordering and stable payload shapes for editor compatibility. 4. Keep docs/examples aligned with `ProgramInfo`-only launch/export flows and `app/` entrypoint layout. diff --git a/Dap.lean b/Dap.lean deleted file mode 100644 index 6316cf6..0000000 --- a/Dap.lean +++ /dev/null @@ -1,21 +0,0 @@ -/- -Copyright (c) 2025 Lean FRO LLC. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Emilio J. Gallego Arias --/ - -import Dap.Lang.Ast -import Dap.Lang.Dsl -import Dap.Lang.Eval -import Dap.Lang.History -import Dap.Lang.Trace -import Dap.Debugger.Session -import Dap.Debugger.Core -import Dap.DAP.Resolve -import Dap.DAP.Launch -import Dap.DAP.Export -import Dap.DAP.Capabilities -import Dap.Widget.Types -import Dap.Widget.UI -import Dap.Widget.Server -import examples.Main diff --git a/ImpLab.lean b/ImpLab.lean new file mode 100644 index 0000000..8138286 --- /dev/null +++ b/ImpLab.lean @@ -0,0 +1,21 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Emilio J. Gallego Arias +-/ + +import ImpLab.Lang.Ast +import ImpLab.Lang.Dsl +import ImpLab.Lang.Eval +import ImpLab.Lang.History +import ImpLab.Lang.Trace +import ImpLab.Debugger.Session +import ImpLab.Debugger.Core +import ImpLab.Debugger.DAP.Resolve +import ImpLab.Debugger.DAP.Launch +import ImpLab.Debugger.DAP.Export +import ImpLab.Debugger.DAP.Capabilities +import ImpLab.Debugger.Widget.Types +import ImpLab.Debugger.Widget.UI +import ImpLab.Debugger.Widget.Server +import examples.Main diff --git a/Dap/Debugger/Core.lean b/ImpLab/Debugger/Core.lean similarity index 99% rename from Dap/Debugger/Core.lean rename to ImpLab/Debugger/Core.lean index c7956b9..1204668 100644 --- a/Dap/Debugger/Core.lean +++ b/ImpLab/Debugger/Core.lean @@ -5,11 +5,11 @@ Author: Emilio J. Gallego Arias -/ import Lean -import Dap.Debugger.Session +import ImpLab.Debugger.Session open Lean -namespace Dap +namespace ImpLab inductive SessionStatus where | stopped @@ -322,4 +322,4 @@ def disconnect (store : SessionStore) (sessionId : Nat) : SessionStore × Bool : def inspectSession (store : SessionStore) (sessionId : Nat) : Except String SessionData := getSessionData store sessionId -end Dap +end ImpLab diff --git a/Dap/DAP/Capabilities.lean b/ImpLab/Debugger/DAP/Capabilities.lean similarity index 93% rename from Dap/DAP/Capabilities.lean rename to ImpLab/Debugger/DAP/Capabilities.lean index fc1962c..a7bd6fd 100644 --- a/Dap/DAP/Capabilities.lean +++ b/ImpLab/Debugger/DAP/Capabilities.lean @@ -8,7 +8,7 @@ import Lean open Lean -namespace Dap +namespace ImpLab structure DapCapabilities where supportsConfigurationDoneRequest : Bool := true @@ -19,4 +19,4 @@ structure DapCapabilities where def dapCapabilities : DapCapabilities := {} -end Dap +end ImpLab diff --git a/Dap/DAP/Export.lean b/ImpLab/Debugger/DAP/Export.lean similarity index 82% rename from Dap/DAP/Export.lean rename to ImpLab/Debugger/DAP/Export.lean index 8c3953b..2d216d5 100644 --- a/Dap/DAP/Export.lean +++ b/ImpLab/Debugger/DAP/Export.lean @@ -5,13 +5,13 @@ Author: Emilio J. Gallego Arias -/ import Lean -import Dap.Lang.Ast -import Dap.DAP.Resolve +import ImpLab.Lang.Ast +import ImpLab.Debugger.DAP.Resolve import examples.Main open Lean -namespace Dap.Export +namespace ImpLab.Export structure CliOptions where decl : String := "mainProgram" @@ -24,13 +24,13 @@ def usage : String := String.intercalate "\n" "", "Export a DAP payload from a Lean declaration.", "", - "--decl must point to a Dap.ProgramInfo declaration.", + "--decl must point to a ImpLab.ProgramInfo declaration.", "", "Default: --decl mainProgram", "Name resolution for unqualified names tries:", " 1) ", " 2) Main.", - " 3) Dap.Lang.Examples." ] + " 3) ImpLab.Lang.Examples." ] private def parseArgs : CliOptions → List String → Except String CliOptions | opts, [] => @@ -55,28 +55,28 @@ private def normalizeDeclName (raw : String) : String := private unsafe def evalProgramInfo (env : Environment) (opts : Options) (decl : Name) : Except String ProgramInfo := do - match env.evalConstCheck ProgramInfo opts ``Dap.ProgramInfo decl with + match env.evalConstCheck ProgramInfo opts ``ImpLab.ProgramInfo decl with | .ok info => info.validate | .error infoErr => - throw s!"Declaration '{decl}' is not Dap.ProgramInfo.\nProgramInfo error: {infoErr}" + throw s!"Declaration '{decl}' is not ImpLab.ProgramInfo.\nProgramInfo error: {infoErr}" private def loadProgramInfoFromDecl (rawDecl : String) : IO ProgramInfo := do let sysroot ← Lean.findSysroot Lean.initSearchPath sysroot [System.FilePath.mk ".lake/build/lib/lean"] let declName ← - match Dap.parseDeclName? rawDecl with + match ImpLab.parseDeclName? rawDecl with | some n => pure n | none => throw <| IO.userError s!"Invalid declaration name '{rawDecl}'" - let env ← Dap.importProjectEnv + let env ← ImpLab.importProjectEnv let opts : Options := {} - let candidates := Dap.candidateDeclNames declName (moduleName? := some `Main) - let resolved? := Dap.resolveFirstDecl? env candidates + let candidates := ImpLab.candidateDeclNames declName (moduleName? := some `Main) + let resolved? := ImpLab.resolveFirstDecl? env candidates let resolved ← match resolved? with | some n => pure n | none => - let attempted := Dap.renderCandidateDecls candidates + let attempted := ImpLab.renderCandidateDecls candidates throw <| IO.userError s!"Could not resolve declaration '{rawDecl}'. Tried: {attempted}" match unsafe evalProgramInfo env opts resolved with | .ok info => pure info @@ -107,4 +107,4 @@ def run (args : List String) : IO Unit := do writeJsonFile opts.out content IO.println s!"Wrote {opts.out} from {normalizeDeclName opts.decl}" -end Dap.Export +end ImpLab.Export diff --git a/Dap/DAP/Launch.lean b/ImpLab/Debugger/DAP/Launch.lean similarity index 89% rename from Dap/DAP/Launch.lean rename to ImpLab/Debugger/DAP/Launch.lean index 2b484cf..eed4773 100644 --- a/Dap/DAP/Launch.lean +++ b/ImpLab/Debugger/DAP/Launch.lean @@ -5,11 +5,11 @@ Author: Emilio J. Gallego Arias -/ import Lean -import Dap.Lang.Ast +import ImpLab.Lang.Ast open Lean -namespace Dap +namespace ImpLab def decodeProgramInfoJson (json : Json) : Except String ProgramInfo := match (fromJson? json : Except String ProgramInfo) with @@ -18,4 +18,4 @@ def decodeProgramInfoJson (json : Json) : Except String ProgramInfo := | .error err => throw s!"Invalid 'programInfo' payload: {err}" -end Dap +end ImpLab diff --git a/Dap/DAP/Resolve.lean b/ImpLab/Debugger/DAP/Resolve.lean similarity index 91% rename from Dap/DAP/Resolve.lean rename to ImpLab/Debugger/DAP/Resolve.lean index 285fafe..b9f89be 100644 --- a/Dap/DAP/Resolve.lean +++ b/ImpLab/Debugger/DAP/Resolve.lean @@ -8,7 +8,7 @@ import Lean open Lean -namespace Dap +namespace ImpLab def parseDeclName? (raw : String) : Option Name := let parts := raw.trimAscii.toString.splitOn "." |>.filter (· != "") @@ -42,7 +42,7 @@ def candidateDeclNames | none => names if includeExamples then - pushIfMissing names (`Dap.Lang.Examples ++ decl) + pushIfMissing names (`ImpLab.Lang.Examples ++ decl) else names else @@ -56,7 +56,7 @@ def renderCandidateDecls (candidates : Array Name) : String := def importProjectEnv : IO Environment := do let candidates : Array (Array Name) := - #[#[`Main, `Dap], #[`Main], #[`Dap]] + #[#[`Main, `ImpLab], #[`Main], #[`ImpLab]] let rec go (idx : Nat) : IO Environment := do if h : idx < candidates.size then let modules := candidates[idx] @@ -66,7 +66,7 @@ def importProjectEnv : IO Environment := do catch _ => go (idx + 1) else - throw <| IO.userError "Could not import project modules (`Main` or `Dap`) to resolve declaration" + throw <| IO.userError "Could not import project modules (`Main` or `ImpLab`) to resolve declaration" go 0 -end Dap +end ImpLab diff --git a/Dap/DAP/Stdio.lean b/ImpLab/Debugger/DAP/Stdio.lean similarity index 93% rename from Dap/DAP/Stdio.lean rename to ImpLab/Debugger/DAP/Stdio.lean index 07ab068..d4d06b1 100644 --- a/Dap/DAP/Stdio.lean +++ b/ImpLab/Debugger/DAP/Stdio.lean @@ -6,13 +6,13 @@ Author: Emilio J. Gallego Arias import Lean import Lean.Data.Lsp.Communication -import Dap.Debugger.Core -import Dap.DAP.Launch -import Dap.DAP.Capabilities +import ImpLab.Debugger.Core +import ImpLab.Debugger.DAP.Launch +import ImpLab.Debugger.DAP.Capabilities open Lean -namespace Dap.ToyDap +namespace ImpLab.Debugger.DAP structure AdapterState where nextSeq : Nat := 1 @@ -118,8 +118,8 @@ private def requireProgramInfo (args : Json) : IO ProgramInfo := do | some json => pure json | none => throw <| IO.userError - "launch requires 'programInfo' (a Dap.ProgramInfo JSON payload)." - match Dap.decodeProgramInfoJson programInfoJson with + "launch requires 'programInfo' (a ImpLab.ProgramInfo JSON payload)." + match ImpLab.decodeProgramInfoJson programInfoJson with | .ok programInfo => pure programInfo | .error err => @@ -169,7 +169,7 @@ private def handleLaunch (stdout : IO.FS.Stream) (stRef : IO.Ref AdapterState) let activeBreakpoints := if breakpoints.isEmpty then pending else breakpoints let st ← stRef.get let (core, launch) ← - match Dap.launchFromProgramInfo st.core programInfo stopOnEntry activeBreakpoints with + match ImpLab.launchFromProgramInfo st.core programInfo stopOnEntry activeBreakpoints with | .ok value => pure value | .error err => throw <| IO.userError err stRef.modify fun st => @@ -203,7 +203,7 @@ private def handleSetBreakpoints (stdout : IO.FS.Stream) (stRef : IO.Ref Adapter sendResponse stdout stRef req <| Json.mkObj [("breakpoints", breakpoints)] | some sessionId => let (core, response) ← - match Dap.setBreakpoints st.core sessionId lines with + match ImpLab.setBreakpoints st.core sessionId lines with | .ok value => pure value | .error err => throw <| IO.userError err stRef.modify fun st => { st with core } @@ -212,7 +212,7 @@ private def handleSetBreakpoints (stdout : IO.FS.Stream) (stRef : IO.Ref Adapter private def handleThreads (stdout : IO.FS.Stream) (stRef : IO.Ref AdapterState) (req : DapRequest) : IO Unit := do - let threads := Dap.threads (← stRef.get).core + let threads := ImpLab.threads (← stRef.get).core let payload := Json.arr <| threads.threads.map fun t => Json.mkObj [("id", toJson t.id), ("name", toJson t.name)] sendResponse stdout stRef req <| Json.mkObj [("threads", payload)] @@ -225,7 +225,7 @@ private def handleStackTrace (stdout : IO.FS.Stream) (stRef : IO.Ref AdapterStat let levels := (args.getObjValAs? Nat "levels").toOption.getD 20 let st ← stRef.get let response ← - match Dap.stackTrace st.core sessionId startFrame levels with + match ImpLab.stackTrace st.core sessionId startFrame levels with | .ok value => pure value | .error err => throw <| IO.userError err let sourceField? := sourceJson? (st.sourcePathBySession.get? sessionId) @@ -248,7 +248,7 @@ private def handleScopes (stdout : IO.FS.Stream) (stRef : IO.Ref AdapterState) let sessionId ← requireSessionId stRef args let frameId := (args.getObjValAs? Nat "frameId").toOption.getD 0 let response ← - match Dap.scopes (← stRef.get).core sessionId frameId with + match ImpLab.scopes (← stRef.get).core sessionId frameId with | .ok value => pure value | .error err => throw <| IO.userError err let scopes := response.scopes.map fun scope => @@ -264,7 +264,7 @@ private def handleVariables (stdout : IO.FS.Stream) (stRef : IO.Ref AdapterState let sessionId ← requireSessionId stRef args let variablesReference := (args.getObjValAs? Nat "variablesReference").toOption.getD 0 let response ← - match Dap.variables (← stRef.get).core sessionId variablesReference with + match ImpLab.variables (← stRef.get).core sessionId variablesReference with | .ok value => pure value | .error err => throw <| IO.userError err let variables := response.variables.map fun var => @@ -278,7 +278,7 @@ private def handleNext (stdout : IO.FS.Stream) (stRef : IO.Ref AdapterState) (req : DapRequest) : IO Unit := do let sessionId ← requireSessionId stRef (requestArgs req) let (core, response) ← - match Dap.next (← stRef.get).core sessionId with + match ImpLab.next (← stRef.get).core sessionId with | .ok value => pure value | .error err => throw <| IO.userError err stRef.modify fun st => { st with core } @@ -289,7 +289,7 @@ private def handleStepIn (stdout : IO.FS.Stream) (stRef : IO.Ref AdapterState) (req : DapRequest) : IO Unit := do let sessionId ← requireSessionId stRef (requestArgs req) let (core, response) ← - match Dap.stepIn (← stRef.get).core sessionId with + match ImpLab.stepIn (← stRef.get).core sessionId with | .ok value => pure value | .error err => throw <| IO.userError err stRef.modify fun st => { st with core } @@ -300,7 +300,7 @@ private def handleStepOut (stdout : IO.FS.Stream) (stRef : IO.Ref AdapterState) (req : DapRequest) : IO Unit := do let sessionId ← requireSessionId stRef (requestArgs req) let (core, response) ← - match Dap.stepOut (← stRef.get).core sessionId with + match ImpLab.stepOut (← stRef.get).core sessionId with | .ok value => pure value | .error err => throw <| IO.userError err stRef.modify fun st => { st with core } @@ -311,7 +311,7 @@ private def handleStepBack (stdout : IO.FS.Stream) (stRef : IO.Ref AdapterState) (req : DapRequest) : IO Unit := do let sessionId ← requireSessionId stRef (requestArgs req) let (core, response) ← - match Dap.stepBack (← stRef.get).core sessionId with + match ImpLab.stepBack (← stRef.get).core sessionId with | .ok value => pure value | .error err => throw <| IO.userError err stRef.modify fun st => { st with core } @@ -322,7 +322,7 @@ private def handleContinue (stdout : IO.FS.Stream) (stRef : IO.Ref AdapterState) (req : DapRequest) : IO Unit := do let sessionId ← requireSessionId stRef (requestArgs req) let (core, response) ← - match Dap.continueExecution (← stRef.get).core sessionId with + match ImpLab.continueExecution (← stRef.get).core sessionId with | .ok value => pure value | .error err => throw <| IO.userError err stRef.modify fun st => { st with core } @@ -336,7 +336,7 @@ private def handlePause (stdout : IO.FS.Stream) (stRef : IO.Ref AdapterState) (req : DapRequest) : IO Unit := do let sessionId ← requireSessionId stRef (requestArgs req) let response ← - match Dap.pause (← stRef.get).core sessionId with + match ImpLab.pause (← stRef.get).core sessionId with | .ok value => pure value | .error err => throw <| IO.userError err sendResponse stdout stRef req @@ -349,7 +349,7 @@ private def handleDisconnect (stdout : IO.FS.Stream) (stRef : IO.Ref AdapterStat let targetSessionId? := (sessionIdFromArgs? args) <|> st.defaultSessionId? let core := match targetSessionId? with - | some sessionId => (Dap.disconnect st.core sessionId).1 + | some sessionId => (ImpLab.disconnect st.core sessionId).1 | none => st.core let sourcePathBySession := match targetSessionId? with @@ -420,4 +420,4 @@ def run : IO Unit := do let stRef ← IO.mkRef ({} : AdapterState) loop stdin stdout stRef -end Dap.ToyDap +end ImpLab.Debugger.DAP diff --git a/Dap/Debugger/Session.lean b/ImpLab/Debugger/Session.lean similarity index 99% rename from Dap/Debugger/Session.lean rename to ImpLab/Debugger/Session.lean index 5dbb2df..bac53a4 100644 --- a/Dap/Debugger/Session.lean +++ b/ImpLab/Debugger/Session.lean @@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Emilio J. Gallego Arias -/ -import Dap.Lang.Eval -import Dap.Lang.History +import ImpLab.Lang.Eval +import ImpLab.Lang.History -namespace Dap +namespace ImpLab inductive StopReason where | entry @@ -271,4 +271,4 @@ def initialStop (session : DebugSession) (stopOnEntry : Bool) : end DebugSession -end Dap +end ImpLab diff --git a/Dap/Widget/Server.lean b/ImpLab/Debugger/Widget/Server.lean similarity index 71% rename from Dap/Widget/Server.lean rename to ImpLab/Debugger/Widget/Server.lean index 448a4f2..0ff0acf 100644 --- a/Dap/Widget/Server.lean +++ b/ImpLab/Debugger/Widget/Server.lean @@ -5,12 +5,12 @@ Author: Emilio J. Gallego Arias -/ import Lean -import Dap.Debugger.Core -import Dap.Widget.Types +import ImpLab.Debugger.Core +import ImpLab.Debugger.Widget.Types open Lean Lean.Server -namespace Dap.Widget.Server +namespace ImpLab.Debugger.Widget.Server initialize dapSessionStoreRef : IO.Ref SessionStore ← IO.mkRef { nextId := 1, sessions := {} } @@ -19,13 +19,13 @@ structure DisconnectResponse where disconnected : Bool deriving Inhabited, Repr, FromJson, ToJson -abbrev WidgetLaunchParams := Dap.TraceWidgetInitProps +abbrev WidgetLaunchParams := ImpLab.TraceWidgetInitProps structure WidgetControlParams where sessionId : Nat deriving Inhabited, Repr, FromJson, ToJson -abbrev WidgetSessionView := Dap.TraceWidgetSessionView +abbrev WidgetSessionView := ImpLab.TraceWidgetSessionView private def mkInvalidParams (message : String) : RequestError := RequestError.invalidParams message @@ -41,15 +41,15 @@ private def updateStore (store : SessionStore) : IO Unit := dapSessionStoreRef.set store private def widgetView (sessionId : Nat) (stopReason : String := "entry") : RequestM WidgetSessionView := do - let data ← runCoreResult <| Dap.inspectSession (← dapSessionStoreRef.get) sessionId - pure <| Dap.TraceWidgetSessionView.ofSessionData sessionId data stopReason + let data ← runCoreResult <| ImpLab.inspectSession (← dapSessionStoreRef.get) sessionId + pure <| ImpLab.TraceWidgetSessionView.ofSessionData sessionId data stopReason @[server_rpc_method] def widgetLaunch (params : WidgetLaunchParams) : RequestM (RequestTask WidgetSessionView) := RequestM.pureTask do let store ← dapSessionStoreRef.get let (store, launch) ← runCoreResult <| - Dap.launchFromProgramInfo store params.programInfo params.stopOnEntry params.breakpoints + ImpLab.launchFromProgramInfo store params.programInfo params.stopOnEntry params.breakpoints updateStore store widgetView launch.sessionId launch.stopReason @@ -57,7 +57,7 @@ def widgetLaunch (params : WidgetLaunchParams) : RequestM (RequestTask WidgetSes def widgetStepIn (params : WidgetControlParams) : RequestM (RequestTask WidgetSessionView) := RequestM.pureTask do let store ← dapSessionStoreRef.get - let (store, control) ← runCoreResult <| Dap.stepIn store params.sessionId + let (store, control) ← runCoreResult <| ImpLab.stepIn store params.sessionId updateStore store widgetView params.sessionId control.stopReason @@ -65,7 +65,7 @@ def widgetStepIn (params : WidgetControlParams) : RequestM (RequestTask WidgetSe def widgetStepBack (params : WidgetControlParams) : RequestM (RequestTask WidgetSessionView) := RequestM.pureTask do let store ← dapSessionStoreRef.get - let (store, control) ← runCoreResult <| Dap.stepBack store params.sessionId + let (store, control) ← runCoreResult <| ImpLab.stepBack store params.sessionId updateStore store widgetView params.sessionId control.stopReason @@ -73,15 +73,15 @@ def widgetStepBack (params : WidgetControlParams) : RequestM (RequestTask Widget def widgetContinue (params : WidgetControlParams) : RequestM (RequestTask WidgetSessionView) := RequestM.pureTask do let store ← dapSessionStoreRef.get - let (store, control) ← runCoreResult <| Dap.continueExecution store params.sessionId + let (store, control) ← runCoreResult <| ImpLab.continueExecution store params.sessionId updateStore store widgetView params.sessionId control.stopReason @[server_rpc_method] def widgetDisconnect (params : WidgetControlParams) : RequestM (RequestTask DisconnectResponse) := RequestM.pureTask do - let (store, disconnected) := Dap.disconnect (← dapSessionStoreRef.get) params.sessionId + let (store, disconnected) := ImpLab.disconnect (← dapSessionStoreRef.get) params.sessionId updateStore store pure { disconnected } -end Dap.Widget.Server +end ImpLab.Debugger.Widget.Server diff --git a/Dap/Widget/Types.lean b/ImpLab/Debugger/Widget/Types.lean similarity index 98% rename from Dap/Widget/Types.lean rename to ImpLab/Debugger/Widget/Types.lean index 0ada2e2..721430a 100644 --- a/Dap/Widget/Types.lean +++ b/ImpLab/Debugger/Widget/Types.lean @@ -5,11 +5,11 @@ Author: Emilio J. Gallego Arias -/ import Lean -import Dap.Debugger.Core +import ImpLab.Debugger.Core open Lean -namespace Dap +namespace ImpLab structure ProgramLineView where functionName : String @@ -97,4 +97,4 @@ def TraceWidgetSessionView.ofSessionData stopReason terminated := data.status = .terminated || data.session.atEnd } -end Dap +end ImpLab diff --git a/Dap/Widget/UI.lean b/ImpLab/Debugger/Widget/UI.lean similarity index 92% rename from Dap/Widget/UI.lean rename to ImpLab/Debugger/Widget/UI.lean index 5a967ba..f322137 100644 --- a/Dap/Widget/UI.lean +++ b/ImpLab/Debugger/Widget/UI.lean @@ -5,11 +5,11 @@ Author: Emilio J. Gallego Arias -/ import Lean -import Dap.Widget.Types +import ImpLab.Debugger.Widget.Types open Lean Widget -namespace Dap +namespace ImpLab @[widget_module] def traceExplorerWidget : Widget.Module where @@ -86,7 +86,7 @@ export default function(props) { setBusy(true); setError(null); try { - const launched = await rs.call('Dap.Widget.Server.widgetLaunch', launchParams); + const launched = await rs.call('ImpLab.Debugger.Widget.Server.widgetLaunch', launchParams); if (!cancelled) { sessionIdRef.current = launched.sessionId; setSession(launched); @@ -101,7 +101,7 @@ export default function(props) { return () => { cancelled = true; if (sessionIdRef.current !== null) { - rs.call('Dap.Widget.Server.widgetDisconnect', { sessionId: sessionIdRef.current }).catch(() => {}); + rs.call('ImpLab.Debugger.Widget.Server.widgetDisconnect', { sessionId: sessionIdRef.current }).catch(() => {}); sessionIdRef.current = null; } }; @@ -232,9 +232,9 @@ export default function(props) { key: 'controls', style: { display: 'flex', gap: '8px', alignItems: 'center', marginBottom: '8px' } }, [ - e('button', { key: 'back', onClick: () => control('Dap.Widget.Server.widgetStepBack'), disabled: busy }, 'StepBack'), - e('button', { key: 'forward', onClick: () => control('Dap.Widget.Server.widgetStepIn'), disabled: busy }, 'StepIn'), - e('button', { key: 'cont', onClick: () => control('Dap.Widget.Server.widgetContinue'), disabled: busy }, 'Continue'), + e('button', { key: 'back', onClick: () => control('ImpLab.Debugger.Widget.Server.widgetStepBack'), disabled: busy }, 'StepBack'), + e('button', { key: 'forward', onClick: () => control('ImpLab.Debugger.Widget.Server.widgetStepIn'), disabled: busy }, 'StepIn'), + e('button', { key: 'cont', onClick: () => control('ImpLab.Debugger.Widget.Server.widgetContinue'), disabled: busy }, 'Continue'), e('span', { key: 'status' }, 'status = ' + String(session.stopReason)), e('span', { key: 'fn', style: { marginLeft: '8px' } }, 'fn = ' + String(state.functionName)), e('span', { key: 'pc', style: { marginLeft: '8px' } }, 'pc = ' + String(state.pc)), @@ -270,4 +270,4 @@ export default function(props) { } " -end Dap +end ImpLab diff --git a/Dap/Lang/Ast.lean b/ImpLab/Lang/Ast.lean similarity index 99% rename from Dap/Lang/Ast.lean rename to ImpLab/Lang/Ast.lean index 6f307c1..28edb54 100644 --- a/Dap/Lang/Ast.lean +++ b/ImpLab/Lang/Ast.lean @@ -8,7 +8,7 @@ import Lean open Lean -namespace Dap +namespace ImpLab /-- Variable names in the toy language. -/ abbrev Var := String @@ -221,4 +221,4 @@ def locationToSourceLine (info : ProgramInfo) (loc : StmtLocation) : Nat := end ProgramInfo -end Dap +end ImpLab diff --git a/Dap/Lang/Dsl.lean b/ImpLab/Lang/Dsl.lean similarity index 99% rename from Dap/Lang/Dsl.lean rename to ImpLab/Lang/Dsl.lean index 2bc99f8..d6bf1b4 100644 --- a/Dap/Lang/Dsl.lean +++ b/ImpLab/Lang/Dsl.lean @@ -5,13 +5,13 @@ Author: Emilio J. Gallego Arias -/ import Lean -import Dap.Lang.Ast +import ImpLab.Lang.Ast open Lean open Lean.Elab open Lean.Elab.Term -namespace Dap +namespace ImpLab declare_syntax_cat dap_rhs declare_syntax_cat dap_stmt @@ -178,4 +178,4 @@ def elabDapProgram : TermElab := fun stx _expectedType? => withRef stx do addTermInfo' stx expr (isDisplayableTerm := true) pure expr -end Dap +end ImpLab diff --git a/Dap/Lang/Eval.lean b/ImpLab/Lang/Eval.lean similarity index 99% rename from Dap/Lang/Eval.lean rename to ImpLab/Lang/Eval.lean index def77c0..ada8b6a 100644 --- a/Dap/Lang/Eval.lean +++ b/ImpLab/Lang/Eval.lean @@ -5,9 +5,9 @@ Author: Emilio J. Gallego Arias -/ import Lean -import Dap.Lang.Ast +import ImpLab.Lang.Ast -namespace Dap +namespace ImpLab abbrev Value := Int abbrev Env := Lean.RBMap Var Value compare @@ -218,4 +218,4 @@ def runFrom (program : Program) (start : Context := Context.initial) : Except Ev def run (program : Program) : Except EvalError Context := runFrom program -end Dap +end ImpLab diff --git a/Dap/Lang/History.lean b/ImpLab/Lang/History.lean similarity index 95% rename from Dap/Lang/History.lean rename to ImpLab/Lang/History.lean index 57d586a..e148bf7 100644 --- a/Dap/Lang/History.lean +++ b/ImpLab/Lang/History.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Emilio J. Gallego Arias -/ -namespace Dap.History +namespace ImpLab.History def maxCursor (items : Array α) : Nat := items.size - 1 @@ -38,4 +38,4 @@ def forwardCursor (items : Array α) (cursor : Nat) : Nat := def jumpCursor (items : Array α) (cursor : Nat) : Nat := normalizeCursor items cursor -end Dap.History +end ImpLab.History diff --git a/Dap/Lang/Trace.lean b/ImpLab/Lang/Trace.lean similarity index 96% rename from Dap/Lang/Trace.lean rename to ImpLab/Lang/Trace.lean index 8abd0eb..fedd7a3 100644 --- a/Dap/Lang/Trace.lean +++ b/ImpLab/Lang/Trace.lean @@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Emilio J. Gallego Arias -/ -import Dap.Lang.Eval -import Dap.Lang.History +import ImpLab.Lang.Eval +import ImpLab.Lang.History -namespace Dap +namespace ImpLab structure ExecutionTrace where program : Program @@ -81,4 +81,4 @@ def jump (explorer : Explorer) (cursor : Nat) : Explorer := end Explorer -end Dap +end ImpLab diff --git a/README.md b/README.md index 5b65eeb..4a72f71 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,4 @@ -# dap +# imp-lab Lean 4 toy debugger project with: - a small function-based toy language, @@ -34,13 +34,13 @@ code client ``` 4. In that VS Code window, press `F5` and choose: -- `Run Lean Toy DAP Extension (watch)` (recommended), or -- `Run Lean Toy DAP Extension (compile once)`. +- `Run ImpLab Toy DAP Extension (watch)` (recommended), or +- `Run ImpLab Toy DAP Extension (compile once)`. 5. In the Extension Development Host that opens: - open this repository, - open `examples/Main.lean`, -- run debug config `Toy DAP (auto-export ProgramInfo)` from `.vscode/launch.json`. +- run debug config `ImpLab Toy DAP (auto-export ProgramInfo)` from `.vscode/launch.json`. - if you need to create/edit one manually, see [VS Code launch process and config](#vs-code-launch-process-and-config). The extension launches `toydap` automatically (default path: `${workspaceFolder}/.lake/build/bin/toydap`). @@ -53,12 +53,12 @@ In a Lean file: ```lean import Lean -import Dap.Widget.UI -import Dap.Widget.Server -import Dap.Widget.Types -import Dap.Lang.Dsl +import ImpLab.Debugger.Widget.UI +import ImpLab.Debugger.Widget.Server +import ImpLab.Debugger.Widget.Types +import ImpLab.Lang.Dsl -open Dap +open ImpLab def mainProgram : ProgramInfo := dap%[ def inc(x) := { @@ -75,7 +75,7 @@ def mainProgram : ProgramInfo := dap%[ def mainProps : TraceWidgetInitProps := { programInfo := mainProgram, stopOnEntry := true } -#widget Dap.traceExplorerWidget with Lean.toJson mainProps +#widget ImpLab.traceExplorerWidget with Lean.toJson mainProps ``` The widget launches a live debugger session and shows grouped function code, current function/pc/source location, call stack, and locals while stepping. @@ -83,7 +83,7 @@ The widget launches a live debugger session and shows grouped function code, cur ### Toy language reference The language has one term elaborator: -- `dap%[...] : Dap.ProgramInfo` +- `dap%[...] : ImpLab.ProgramInfo` `dap%[...]` accepts only function definitions and must include `main()` as entrypoint. @@ -102,7 +102,7 @@ return v Example: ```lean -def p : Dap.ProgramInfo := dap%[ +def p : ImpLab.ProgramInfo := dap%[ def addMul(x, y) := { let s := add x y, let z := mul s y, @@ -128,7 +128,7 @@ A launch config is a VS Code debug profile (JSON in `launch.json`) that tells VS - which inputs to pass (`programInfo`, `source`, `stopOnEntry`, etc.). Launch flow in this repository: -1. You run `Toy DAP (auto-export ProgramInfo)` from `.vscode/launch.json`. +1. You run `ImpLab Toy DAP (auto-export ProgramInfo)` from `.vscode/launch.json`. 2. Its `preLaunchTask` runs `dap-export` and writes `.dap/programInfo.generated.json`. 3. The extension launches `toydap`. 4. If `programInfo` is not inline in launch JSON, the extension auto-loads `.dap/programInfo.generated.json`. @@ -137,7 +137,7 @@ Minimal config (customize as needed): ```json { - "name": "Lean Toy DAP", + "name": "ImpLab Toy DAP", "type": "lean-toy-dap", "request": "launch", "source": "${file}", @@ -157,7 +157,7 @@ Notes: Manual export (advanced/internal): generate source-aware JSON from a Lean declaration: ```bash -lake exe dap-export --decl Dap.Lang.Examples.mainProgram --out .dap/programInfo.generated.json +lake exe dap-export --decl ImpLab.Lang.Examples.mainProgram --out .dap/programInfo.generated.json ``` Using a different declaration than `mainProgram`: @@ -168,7 +168,7 @@ lake exe dap-export --decl MyProject.Debugger.lesson1Program --out .dap/programI Then launch normally from VS Code; the extension will pick up the newly generated `.dap/programInfo.generated.json`. -`--decl` must resolve to a `Dap.ProgramInfo` declaration. +`--decl` must resolve to an `ImpLab.ProgramInfo` declaration. `toydap` CLI arguments (`lake exe toydap --help`): - No CLI flags are currently supported. @@ -190,12 +190,12 @@ The interpreter uses explicit call frames: ### Lean RPC widget methods -Registered in `Dap.Widget.Server`: -- `Dap.Widget.Server.widgetLaunch` -- `Dap.Widget.Server.widgetStepIn` -- `Dap.Widget.Server.widgetStepBack` -- `Dap.Widget.Server.widgetContinue` -- `Dap.Widget.Server.widgetDisconnect` +Registered in `ImpLab.Debugger.Widget.Server`: +- `ImpLab.Debugger.Widget.Server.widgetLaunch` +- `ImpLab.Debugger.Widget.Server.widgetStepIn` +- `ImpLab.Debugger.Widget.Server.widgetStepBack` +- `ImpLab.Debugger.Widget.Server.widgetContinue` +- `ImpLab.Debugger.Widget.Server.widgetDisconnect` `widgetLaunch` accepts `programInfo` plus optional `stopOnEntry` and `breakpoints`. @@ -204,20 +204,20 @@ Registered in `Dap.Widget.Server`: - `app/` executables: - `app/ToyDap.lean`: stdio DAP adapter entrypoint (`lake exe toydap`). - `app/ExportMain.lean`: `ProgramInfo` export CLI (`lake exe dap-export`). - - These files are intentional thin entrypoints; logic lives under `Dap/*`. -- `Dap/Lang/Ast.lean`: core AST (`Program` is a list of functions, entrypoint is `main`). -- `Dap/Lang/Dsl.lean`: DSL syntax/macros (`dap%[...]`) + infotree metadata. -- `Dap/Lang/Eval.lean`: environment, call-stack semantics, small-step transition, and full runner. -- `Dap/Lang/History.lean`: shared cursor/history navigation helpers. -- `Dap/Lang/Trace.lean`: execution trace and navigation API (`Explorer`). + - These files are intentional thin entrypoints; logic lives under `ImpLab/*`. +- `ImpLab/Lang/Ast.lean`: core AST (`Program` is a list of functions, entrypoint is `main`). +- `ImpLab/Lang/Dsl.lean`: DSL syntax/macros (`dap%[...]`) + infotree metadata. +- `ImpLab/Lang/Eval.lean`: environment, call-stack semantics, small-step transition, and full runner. +- `ImpLab/Lang/History.lean`: shared cursor/history navigation helpers. +- `ImpLab/Lang/Trace.lean`: execution trace and navigation API (`Explorer`). - `examples/Main.lean`: sample program and widget launch props. -- `Dap/Debugger/Session.lean`: pure debugger session model (breakpoints, continue, next, stepIn, stepOut, stepBack). -- `Dap/Debugger/Core.lean`: session store + DAP-shaped pure core operations. -- `Dap/Widget/Server.lean`: Lean server RPC endpoints implementing DAP-like operations. -- `Dap/DAP/Stdio.lean`: standalone DAP adapter implementation (native DAP protocol over stdio). -- `Dap/Widget/Types.lean`: widget launch/session view models and session-to-widget projection helpers. -- `Dap/Widget/UI.lean`: `traceExplorerWidget` module UI. -- `Dap/DAP/Export.lean`: `dap-export` declaration loader/export logic. +- `ImpLab/Debugger/Session.lean`: pure debugger session model (breakpoints, continue, next, stepIn, stepOut, stepBack). +- `ImpLab/Debugger/Core.lean`: session store + DAP-shaped pure core operations. +- `ImpLab/Debugger/Widget/Server.lean`: Lean server RPC endpoints implementing DAP-like operations. +- `ImpLab/Debugger/DAP/Stdio.lean`: standalone DAP adapter implementation (native DAP protocol over stdio). +- `ImpLab/Debugger/Widget/Types.lean`: widget launch/session view models and session-to-widget projection helpers. +- `ImpLab/Debugger/Widget/UI.lean`: `traceExplorerWidget` module UI. +- `ImpLab/Debugger/DAP/Export.lean`: `dap-export` declaration loader/export logic. - `Test/Core.lean`: core/runtime/debugger tests. - `Test/Transport.lean`: DAP stdio transport lifecycle/framing tests. - `Test/Main.lean`: test runner executable. diff --git a/Test/Core.lean b/Test/Core.lean index c90bd2d..608aa6c 100644 --- a/Test/Core.lean +++ b/Test/Core.lean @@ -6,10 +6,10 @@ Author: Emilio J. Gallego Arias import Test.Util -open Dap +open ImpLab open Lean -namespace Dap.Tests +namespace ImpLab.Tests private def mkProgram (mainBody : Array Stmt) (helpers : Array FuncDef := #[]) : Program := { functions := #[{ name := Program.mainName, params := #[], body := mainBody }] ++ helpers } @@ -184,8 +184,8 @@ def testWidgetProps : IO Unit := do Stmt.letBin "z" .div "y" "x" ] let info := mkProgramInfo program - let (store, launch) ← expectCore "widget launch" <| Dap.launchFromProgramInfo {} info true #[] - let data ← expectCore "widget session inspect" <| Dap.inspectSession store launch.sessionId + let (store, launch) ← expectCore "widget launch" <| ImpLab.launchFromProgramInfo {} info true #[] + let data ← expectCore "widget session inspect" <| ImpLab.inspectSession store launch.sessionId let props := TraceWidgetSessionView.ofSessionData launch.sessionId data launch.stopReason assertEq "widget session id" props.sessionId launch.sessionId assertEq "widget program length" props.program.size program.totalStmtCount @@ -200,9 +200,9 @@ def testWidgetSessionProjectionAfterStep : IO Unit := do let z := div y x } ] - let (store1, launch) ← expectCore "widget step launch" <| Dap.launchFromProgramInfo {} info true #[] - let (store2, step) ← expectCore "widget step forward" <| Dap.stepIn store1 launch.sessionId - let data ← expectCore "widget step inspect" <| Dap.inspectSession store2 launch.sessionId + let (store1, launch) ← expectCore "widget step launch" <| ImpLab.launchFromProgramInfo {} info true #[] + let (store2, step) ← expectCore "widget step forward" <| ImpLab.stepIn store1 launch.sessionId + let data ← expectCore "widget step inspect" <| ImpLab.inspectSession store2 launch.sessionId let props := TraceWidgetSessionView.ofSessionData launch.sessionId data step.stopReason assertEq "widget step reason propagated" props.stopReason step.stopReason assertEq "widget step state pc" props.state.pc 1 @@ -214,12 +214,12 @@ def testStepBackAfterTermination : IO Unit := do let x := 1 } ] - let (store1, launch) ← expectCore "stepBack term launch" <| Dap.launchFromProgramInfo {} info false #[] + let (store1, launch) ← expectCore "stepBack term launch" <| ImpLab.launchFromProgramInfo {} info false #[] assertEq "stepBack term launch terminated" launch.terminated true - let (store2, back) ← expectCore "stepBack term backward" <| Dap.stepBack store1 launch.sessionId + let (store2, back) ← expectCore "stepBack term backward" <| ImpLab.stepBack store1 launch.sessionId assertEq "stepBack term reason" back.stopReason "step" assertEq "stepBack term terminated false" back.terminated false - let data ← expectCore "stepBack term inspect" <| Dap.inspectSession store2 launch.sessionId + let data ← expectCore "stepBack term inspect" <| ImpLab.inspectSession store2 launch.sessionId assertEq "stepBack term cursor rewound" data.session.currentPc 0 def testWidgetInitProps : IO Unit := do @@ -326,35 +326,35 @@ def testDebugCoreStepInOut : IO Unit := do } ] let store0 : SessionStore := {} - let (store1, launch) ← expectCore "step in/out launch" <| Dap.launchFromProgramInfo store0 info true #[] + let (store1, launch) ← expectCore "step in/out launch" <| ImpLab.launchFromProgramInfo store0 info true #[] assertEq "step in/out launch reason" launch.stopReason "entry" let sessionId := launch.sessionId - let (store2, _) ← expectCore "step in/out main step 1" <| Dap.stepIn store1 sessionId - let (store3, _) ← expectCore "step in/out enter outer" <| Dap.stepIn store2 sessionId - let stackOuter ← expectCore "step in/out stack outer" <| Dap.stackTrace store3 sessionId + let (store2, _) ← expectCore "step in/out main step 1" <| ImpLab.stepIn store1 sessionId + let (store3, _) ← expectCore "step in/out enter outer" <| ImpLab.stepIn store2 sessionId + let stackOuter ← expectCore "step in/out stack outer" <| ImpLab.stackTrace store3 sessionId assertEq "step in/out depth after entering outer" stackOuter.totalFrames 2 assertTrue "step in/out top frame is outer" ((stackOuter.stackFrames[0]?.map (·.name.contains "outer")).getD false) - let (store4, _) ← expectCore "step in/out enter inner" <| Dap.stepIn store3 sessionId - let stackInner ← expectCore "step in/out stack inner" <| Dap.stackTrace store4 sessionId + let (store4, _) ← expectCore "step in/out enter inner" <| ImpLab.stepIn store3 sessionId + let stackInner ← expectCore "step in/out stack inner" <| ImpLab.stackTrace store4 sessionId assertEq "step in/out depth after entering inner" stackInner.totalFrames 3 assertTrue "step in/out top frame is inner" ((stackInner.stackFrames[0]?.map (·.name.contains "inner")).getD false) - let (store5, outInner) ← expectCore "step in/out return from inner" <| Dap.stepOut store4 sessionId + let (store5, outInner) ← expectCore "step in/out return from inner" <| ImpLab.stepOut store4 sessionId assertEq "step in/out return from inner reason" outInner.stopReason "step" assertEq "step in/out return from inner terminated" outInner.terminated false - let stackAfterInner ← expectCore "step in/out stack after inner" <| Dap.stackTrace store5 sessionId + let stackAfterInner ← expectCore "step in/out stack after inner" <| ImpLab.stackTrace store5 sessionId assertEq "step in/out depth after inner return" stackAfterInner.totalFrames 2 assertTrue "step in/out top frame returns to outer" ((stackAfterInner.stackFrames[0]?.map (·.name.contains "outer")).getD false) - let (store6, outOuter) ← expectCore "step in/out return from outer" <| Dap.stepOut store5 sessionId + let (store6, outOuter) ← expectCore "step in/out return from outer" <| ImpLab.stepOut store5 sessionId assertEq "step in/out return from outer reason" outOuter.stopReason "step" assertEq "step in/out return from outer terminated" outOuter.terminated false - let stackAfterOuter ← expectCore "step in/out stack after outer" <| Dap.stackTrace store6 sessionId + let stackAfterOuter ← expectCore "step in/out stack after outer" <| ImpLab.stackTrace store6 sessionId assertEq "step in/out depth after outer return" stackAfterOuter.totalFrames 1 assertTrue "step in/out top frame returns to main" ((stackAfterOuter.stackFrames[0]?.map (·.name.contains "main")).getD false) - let (_store7, outMain) ← expectCore "step in/out return from main" <| Dap.stepOut store6 sessionId + let (_store7, outMain) ← expectCore "step in/out return from main" <| ImpLab.stepOut store6 sessionId assertEq "step in/out return from main reason" outMain.stopReason "terminated" assertEq "step in/out return from main terminated" outMain.terminated true @@ -372,16 +372,16 @@ def testDebugCoreNextStepsOverCall : IO Unit := do } ] let store0 : SessionStore := {} - let (store1, launch) ← expectCore "step over launch" <| Dap.launchFromProgramInfo store0 info true #[] + let (store1, launch) ← expectCore "step over launch" <| ImpLab.launchFromProgramInfo store0 info true #[] assertEq "step over launch reason" launch.stopReason "entry" let sessionId := launch.sessionId - let (store2, _) ← expectCore "step over next 1" <| Dap.next store1 sessionId - let (store3, nextOver) ← expectCore "step over call" <| Dap.next store2 sessionId + let (store2, _) ← expectCore "step over next 1" <| ImpLab.next store1 sessionId + let (store3, nextOver) ← expectCore "step over call" <| ImpLab.next store2 sessionId assertEq "step over call reason" nextOver.stopReason "step" assertEq "step over call terminated" nextOver.terminated false - let stackAfterCall ← expectCore "step over stack after call" <| Dap.stackTrace store3 sessionId + let stackAfterCall ← expectCore "step over stack after call" <| ImpLab.stackTrace store3 sessionId assertEq "step over stays in caller frame" stackAfterCall.totalFrames 1 - let vars ← expectCore "step over vars after call" <| Dap.variables store3 sessionId 1 + let vars ← expectCore "step over vars after call" <| ImpLab.variables store3 sessionId 1 assertTrue "step over computed call result in caller" (vars.variables.any fun v => v.name == "b" && v.value == "8") @@ -480,19 +480,19 @@ def testDebugCoreFlow : IO Unit := do ] let bpLine := info.locationToSourceLine { func := Program.mainName, stmtLine := 2 } let store0 : SessionStore := {} - let (store1, launch) ← expectCore "core launch" <| Dap.launchFromProgramInfo store0 info false #[bpLine] + let (store1, launch) ← expectCore "core launch" <| ImpLab.launchFromProgramInfo store0 info false #[bpLine] assertEq "core launch stopReason" launch.stopReason "breakpoint" assertEq "core launch line" launch.line bpLine let sessionId := launch.sessionId - let vars1 ← expectCore "core vars" <| Dap.variables store1 sessionId 1 + let vars1 ← expectCore "core vars" <| ImpLab.variables store1 sessionId 1 assertTrue "core vars contain x binding" (vars1.variables.any fun v => v.name == "x" && v.value == "5") - let (store2, cont) ← expectCore "core continue" <| Dap.continueExecution store1 sessionId + let (store2, cont) ← expectCore "core continue" <| ImpLab.continueExecution store1 sessionId assertEq "core continue terminated" cont.terminated true assertEq "core continue stopReason" cont.stopReason "terminated" - let (store3, disconnected) := Dap.disconnect store2 sessionId + let (store3, disconnected) := ImpLab.disconnect store2 sessionId assertEq "core disconnect" disconnected true - let pauseAfterDisconnect := Dap.pause store3 sessionId + let pauseAfterDisconnect := ImpLab.pause store3 sessionId match pauseAfterDisconnect with | .ok _ => throw <| IO.userError "core pause after disconnect should fail" @@ -513,24 +513,24 @@ def testDebugCoreStackFrames : IO Unit := do } ] let store0 : SessionStore := {} - let (store1, launch) ← expectCore "stack frames launch" <| Dap.launchFromProgramInfo store0 info true #[] + let (store1, launch) ← expectCore "stack frames launch" <| ImpLab.launchFromProgramInfo store0 info true #[] assertEq "stack frames launch stopReason" launch.stopReason "entry" let sessionId := launch.sessionId - let (store2, _) ← expectCore "stack frames next 1" <| Dap.next store1 sessionId - let (store3, _) ← expectCore "stack frames next 2" <| Dap.next store2 sessionId - let (store4, _) ← expectCore "stack frames stepIn call" <| Dap.stepIn store3 sessionId - let stack ← expectCore "stack frames stackTrace" <| Dap.stackTrace store4 sessionId + let (store2, _) ← expectCore "stack frames next 1" <| ImpLab.next store1 sessionId + let (store3, _) ← expectCore "stack frames next 2" <| ImpLab.next store2 sessionId + let (store4, _) ← expectCore "stack frames stepIn call" <| ImpLab.stepIn store3 sessionId + let stack ← expectCore "stack frames stackTrace" <| ImpLab.stackTrace store4 sessionId assertEq "stack frames total" stack.totalFrames 2 let top := stack.stackFrames[0]?.getD default let caller := stack.stackFrames[1]?.getD default assertTrue "stack frames top is callee" (top.name.contains "addMul") assertTrue "stack frames caller is main" (caller.name.contains "main") - let scopesTop ← expectCore "stack frames scopes top" <| Dap.scopes store4 sessionId 0 + let scopesTop ← expectCore "stack frames scopes top" <| ImpLab.scopes store4 sessionId 0 assertEq "stack frames top scope count" scopesTop.scopes.size 1 - let varsTop ← expectCore "stack frames vars top" <| Dap.variables store4 sessionId 1 + let varsTop ← expectCore "stack frames vars top" <| ImpLab.variables store4 sessionId 1 assertTrue "stack frames top vars include x" (varsTop.variables.any fun v => v.name == "x" && v.value == "2") - let varsCaller ← expectCore "stack frames vars caller" <| Dap.variables store4 sessionId 2 + let varsCaller ← expectCore "stack frames vars caller" <| ImpLab.variables store4 sessionId 2 assertTrue "stack frames caller vars include a" (varsCaller.variables.any fun v => v.name == "a" && v.value == "2") @@ -541,11 +541,11 @@ def testDebugCoreTerminatedGuards : IO Unit := do } ] let store0 : SessionStore := {} - let (store1, launch) ← expectCore "terminated guards launch" <| Dap.launchFromProgramInfo store0 info false #[] + let (store1, launch) ← expectCore "terminated guards launch" <| ImpLab.launchFromProgramInfo store0 info false #[] assertEq "terminated guards launch terminated" launch.terminated true let sessionId := launch.sessionId - let nextAfterTerminated := Dap.next store1 sessionId - let setBpAfterTerminated := Dap.setBreakpoints store1 sessionId #[1] + let nextAfterTerminated := ImpLab.next store1 sessionId + let setBpAfterTerminated := ImpLab.setBreakpoints store1 sessionId #[1] match nextAfterTerminated with | .ok _ => throw <| IO.userError "next should fail on terminated session" @@ -563,7 +563,7 @@ def testDebugCoreRejectsInvalidProgramInfo : IO Unit := do let invalid : ProgramInfo := { program := { functions := #[{ name := "helper", params := #[], body := #[stmt] }] } located := #[{ func := "helper", stmtLine := 1, stmt, span }] } - let launch := Dap.launchFromProgramInfo (store := {}) invalid true #[] + let launch := ImpLab.launchFromProgramInfo (store := {}) invalid true #[] match launch with | .ok _ => throw <| IO.userError "launch should fail with invalid ProgramInfo" @@ -571,15 +571,15 @@ def testDebugCoreRejectsInvalidProgramInfo : IO Unit := do assertTrue "invalid program info launch error mentions main" (err.contains "main") def testResolveCandidateDeclNames : IO Unit := do - let unqualified := Dap.candidateDeclNames `mainProgram (moduleName? := some `Main) + let unqualified := ImpLab.candidateDeclNames `mainProgram (moduleName? := some `Main) assertEq "candidate names include local module and examples" unqualified - #[`mainProgram, `Main.mainProgram, `Dap.Lang.Examples.mainProgram] - let dedup := Dap.candidateDeclNames `mainProgram (moduleName? := some `Dap.Lang.Examples) + #[`mainProgram, `Main.mainProgram, `ImpLab.Lang.Examples.mainProgram] + let dedup := ImpLab.candidateDeclNames `mainProgram (moduleName? := some `ImpLab.Lang.Examples) assertEq "candidate names are deduplicated" dedup - #[`mainProgram, `Dap.Lang.Examples.mainProgram] - let qualified := Dap.candidateDeclNames `Main.mainProgram (moduleName? := some `Main) + #[`mainProgram, `ImpLab.Lang.Examples.mainProgram] + let qualified := ImpLab.candidateDeclNames `Main.mainProgram (moduleName? := some `Main) assertEq "qualified names stay unchanged" qualified #[`Main.mainProgram] def runCoreTests : IO Unit := do @@ -612,4 +612,4 @@ def runCoreTests : IO Unit := do testDebugCoreRejectsInvalidProgramInfo testResolveCandidateDeclNames -end Dap.Tests +end ImpLab.Tests diff --git a/Test/Main.lean b/Test/Main.lean index ca77bc0..4c7ece0 100644 --- a/Test/Main.lean +++ b/Test/Main.lean @@ -8,6 +8,6 @@ import Test.Core import Test.Transport def main : IO Unit := do - Dap.Tests.runCoreTests - Dap.Tests.runTransportTests + ImpLab.Tests.runCoreTests + ImpLab.Tests.runTransportTests IO.println "All tests passed." diff --git a/Test/Transport.lean b/Test/Transport.lean index 97000c5..1e90d7d 100644 --- a/Test/Transport.lean +++ b/Test/Transport.lean @@ -6,10 +6,10 @@ Author: Emilio J. Gallego Arias import Test.Util -open Dap +open ImpLab open Lean -namespace Dap.Tests +namespace ImpLab.Tests private def encodeDapRequest (seq : Nat) (command : String) (arguments : Json := Json.mkObj []) : String := let payload := Json.mkObj @@ -44,11 +44,11 @@ private def appearsBefore (s first second : String) : Bool := private def launchArgs (stopOnEntry : Bool) : Json := Json.mkObj - [ ("programInfo", toJson Dap.Lang.Examples.mainProgram), + [ ("programInfo", toJson ImpLab.Lang.Examples.mainProgram), ("stopOnEntry", toJson stopOnEntry) ] private def bumpEntryLine : Nat := - Dap.Lang.Examples.mainProgram.locationToSourceLine { func := "bump", stmtLine := 1 } + ImpLab.Lang.Examples.mainProgram.locationToSourceLine { func := "bump", stmtLine := 1 } def testToyDapProtocolSanity : IO Unit := do let stdinPayload := @@ -239,4 +239,4 @@ def runTransportTests : IO Unit := do testToyDapLaunchTerminatesOrder testToyDapDisconnectCanTargetSessionId -end Dap.Tests +end ImpLab.Tests diff --git a/Test/Util.lean b/Test/Util.lean index c239dcf..4f0c48a 100644 --- a/Test/Util.lean +++ b/Test/Util.lean @@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Emilio J. Gallego Arias -/ -import Dap +import ImpLab -namespace Dap.Tests +namespace ImpLab.Tests def assertEq [BEq α] [ToString α] (label : String) (actual expected : α) : IO Unit := do if actual == expected then @@ -32,4 +32,4 @@ def expectCore (label : String) (result : Except String α) : IO α := do | .error err => throw <| IO.userError s!"{label}: {err}" -end Dap.Tests +end ImpLab.Tests diff --git a/app/ExportMain.lean b/app/ExportMain.lean index fa51346..dcdb77b 100644 --- a/app/ExportMain.lean +++ b/app/ExportMain.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Emilio J. Gallego Arias -/ -import Dap.DAP.Export +import ImpLab.Debugger.DAP.Export def main (args : List String) : IO Unit := do - Dap.Export.run args + ImpLab.Export.run args diff --git a/app/ToyDap.lean b/app/ToyDap.lean index 4af34c2..a4b56a1 100644 --- a/app/ToyDap.lean +++ b/app/ToyDap.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Emilio J. Gallego Arias -/ -import Dap.DAP.Stdio +import ImpLab.Debugger.DAP.Stdio def main : IO Unit := do - Dap.ToyDap.run + ImpLab.Debugger.DAP.run diff --git a/client/README.md b/client/README.md index 8f89b16..27881fd 100644 --- a/client/README.md +++ b/client/README.md @@ -1,4 +1,4 @@ -# Lean Toy DAP Client (VS Code) +# ImpLab Toy DAP Client (VS Code) This extension starts the standalone `toydap` debug adapter binary built from this repository. @@ -30,7 +30,7 @@ Use debug type `lean-toy-dap`. - Optional source path shown in stack traces. Launch payload: -- `programInfo`: `Dap.ProgramInfo` JSON payload. +- `programInfo`: `ImpLab.ProgramInfo` JSON payload. - If omitted, the extension tries `${workspaceFolder}/.dap/programInfo.generated.json`. - The extension does not auto-load `client/programInfo.sample.json`; that file is only a reference shape. @@ -42,13 +42,13 @@ Example: ```json { - "name": "Lean Toy DAP", + "name": "ImpLab Toy DAP", "type": "lean-toy-dap", "request": "launch", "source": "${file}", "toydapPath": "${workspaceFolder}/.lake/build/bin/toydap", "programInfo": { - "...": "Dap.ProgramInfo JSON" + "...": "ImpLab.ProgramInfo JSON" }, "stopOnEntry": true } diff --git a/client/package.json b/client/package.json index 9699038..a52cc40 100644 --- a/client/package.json +++ b/client/package.json @@ -1,6 +1,6 @@ { "name": "lean-toy-dap-client", - "displayName": "Lean Toy DAP Client", + "displayName": "ImpLab Toy DAP Client", "description": "Side-loadable VS Code extension for the standalone toydap debug adapter binary.", "version": "0.0.1", "publisher": "local", @@ -13,14 +13,14 @@ ], "activationEvents": [ "onDebug", - "onCommand:leanToyDap.startDebugging" + "onCommand:impLab.startDebugging" ], "main": "./out/extension.js", "contributes": { "commands": [ { - "command": "leanToyDap.startDebugging", - "title": "Lean Toy DAP: Start Debugging" + "command": "impLab.startDebugging", + "title": "ImpLab Toy DAP: Start Debugging" } ], "breakpoints": [ @@ -34,7 +34,7 @@ "debuggers": [ { "type": "lean-toy-dap", - "label": "Lean Toy DAP", + "label": "ImpLab Toy DAP", "languages": [ "lean", "lean4" @@ -53,7 +53,7 @@ }, "programInfo": { "type": "object", - "description": "Source-aware payload (`Dap.ProgramInfo`) including function-aware statement spans for source mapping." + "description": "Source-aware payload (`ImpLab.ProgramInfo`) including function-aware statement spans for source mapping." }, "toydapPath": { "type": "string", @@ -75,16 +75,16 @@ }, "configurationSnippets": [ { - "label": "Lean Toy DAP", + "label": "ImpLab Toy DAP", "description": "Debug the toy arithmetic language through the standalone toydap binary", "body": { - "name": "Lean Toy DAP", + "name": "ImpLab Toy DAP", "type": "lean-toy-dap", "request": "launch", "source": "${file}", "toydapPath": "${workspaceFolder}/.lake/build/bin/toydap", "programInfo": { - "...": "Dap.ProgramInfo JSON" + "...": "ImpLab.ProgramInfo JSON" }, "stopOnEntry": true } diff --git a/client/src/extension.ts b/client/src/extension.ts index 4c0f068..ec0a7ee 100644 --- a/client/src/extension.ts +++ b/client/src/extension.ts @@ -60,7 +60,7 @@ class LeanToyDebugConfigurationProvider implements vscode.DebugConfigurationProv config.request = 'launch' } if (!config.name) { - config.name = 'Lean Toy DAP' + config.name = 'ImpLab Toy DAP' } if (!config.source) { const active = vscode.window.activeTextEditor?.document.uri @@ -97,7 +97,7 @@ class LeanToyDebugConfigurationProvider implements vscode.DebugConfigurationProv } export function activate(context: vscode.ExtensionContext): void { - const output = vscode.window.createOutputChannel('Lean Toy DAP') + const output = vscode.window.createOutputChannel('ImpLab Toy DAP') const configProvider = new LeanToyDebugConfigurationProvider(output) const adapterFactory = new LeanToyDebugAdapterFactory(output) @@ -106,11 +106,11 @@ export function activate(context: vscode.ExtensionContext): void { output, vscode.debug.registerDebugConfigurationProvider('lean-toy-dap', configProvider), vscode.debug.registerDebugAdapterDescriptorFactory('lean-toy-dap', adapterFactory), - vscode.commands.registerCommand('leanToyDap.startDebugging', async () => { + vscode.commands.registerCommand('impLab.startDebugging', async () => { const active = vscode.window.activeTextEditor?.document.uri const source = active?.scheme === 'file' ? active.fsPath : undefined await vscode.debug.startDebugging(undefined, { - name: 'Lean Toy DAP', + name: 'ImpLab Toy DAP', type: 'lean-toy-dap', request: 'launch', source, diff --git a/examples/Main.lean b/examples/Main.lean index 4b9b3f8..1a50a9d 100644 --- a/examples/Main.lean +++ b/examples/Main.lean @@ -4,13 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Emilio J. Gallego Arias -/ -import Dap.Widget.UI -import Dap.Lang.Dsl -import Dap.Widget.Server +import ImpLab.Debugger.Widget.UI +import ImpLab.Lang.Dsl +import ImpLab.Debugger.Widget.Server -namespace Dap.Lang.Examples +namespace ImpLab.Lang.Examples -open Dap +open ImpLab def mainProgram : ProgramInfo := dap%[ def bump(x) := { @@ -40,6 +40,6 @@ def sampleTraceProps : TraceWidgetInitProps := def sampleTracePropsJson : Lean.Json := Lean.toJson sampleTraceProps -end Dap.Lang.Examples +end ImpLab.Lang.Examples -#widget Dap.traceExplorerWidget with Dap.Lang.Examples.sampleTracePropsJson +#widget ImpLab.traceExplorerWidget with ImpLab.Lang.Examples.sampleTracePropsJson diff --git a/dap.code-workspace b/implab.code-workspace similarity index 100% rename from dap.code-workspace rename to implab.code-workspace diff --git a/lakefile.toml b/lakefile.toml index 819e40e..84fee99 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -1,9 +1,9 @@ -name = "dap" +name = "implab" version = "0.1.0" defaultTargets = ["toydap", "dap-tests"] [[lean_lib]] -name = "Dap" +name = "ImpLab" [[lean_lib]] name = "examples" From baa6cfb4d8c02d728a6169a5c17039d87bbacdd4 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 24 Feb 2026 21:44:47 +0100 Subject: [PATCH 2/9] Split debugger docs and move debugger agent rules locally --- AGENTS.md | 35 ++----- ImpLab/Debugger/AGENTS.md | 29 +++++ README.md | 215 +++++--------------------------------- docs/debugger.md | 80 ++++++++++++++ 4 files changed, 142 insertions(+), 217 deletions(-) create mode 100644 ImpLab/Debugger/AGENTS.md create mode 100644 docs/debugger.md diff --git a/AGENTS.md b/AGENTS.md index 87c416f..8337762 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -1,16 +1,15 @@ # AGENTS ## Scope and priorities -- Educational Lean 4 toy language + debugger. +- Educational Lean 4 playground for language modeling and debugger experimentation. - Optimize for clarity and maintainability, not performance. - Avoid compatibility shims during refactors; prefer direct clean structure. ## Main surfaces -- Runtime: `ImpLab/Lang/*.lean` -- Debugger source of truth: `ImpLab/Debugger/Core.lean` -- Session semantics: `ImpLab/Debugger/Session.lean` -- Lean RPC transport: `ImpLab/Debugger/Widget/Server.lean` -- StdIO DAP transport: `ImpLab/Debugger/DAP/Stdio.lean` + `app/ToyDap.lean` +- Language runtime and semantics: `ImpLab/Lang/*.lean` +- Debugger subsystem: `ImpLab/Debugger/*` +- Executables: `app/` +- Tests: `Test/` - VS Code client: `client/` ## Build/test commands @@ -20,28 +19,12 @@ - `lake exe dap-export --help` - `cd client && npm run compile` -## Architecture guardrails -- Put new debugger behavior in `ImpLab/Debugger/Core.lean` first, then wire transports. -- Keep transport files as adapters only; avoid protocol/state duplication. -- Treat `ProgramInfo` as canonical across launch/debug/export flows. -- `Program` remains function-only (`functions : Array FuncDef`) with required `main`. -- Keep source mapping coherent (function + statement line <-> source line). - -## Language and API conventions +## Global conventions - `dap%[...]` is the only DSL elaborator and must produce `ProgramInfo`. - `dap%[...]` accepts functions only and must include `main()` (zero params). - Keep `mainProgram` as default fixture entrypoint in `examples/Main.lean`. - Prefer `initialize` over `builtin_initialize` in project code. -- Preserve stable DAP JSON payload shapes. - -## Testing split -- Core behavior tests: `ImpLab/Debugger/Core.lean` APIs. -- Transport tests: framing/serialization + request-to-core wiring. -- DAP sanity tests: lifecycle ordering + at least one breakpoint hit path. -## Review checklist -- Is behavior duplicated in `Server.lean`/`Stdio.lean` that belongs in core? -- Any hardcoded entrypoint/decl list that should be generalized? -- Any duplicated decode/source-mapping logic that can drift? -- Are stack/breakpoint lines mapped correctly for all functions via `ProgramInfo`? -- Are lifecycle events ordered correctly (`initialized`, `stopped`, `continued`, `terminated`)? +## Subsystem-local instructions +- Debugger-specific rules and review checklist live in: + - `ImpLab/Debugger/AGENTS.md` diff --git a/ImpLab/Debugger/AGENTS.md b/ImpLab/Debugger/AGENTS.md new file mode 100644 index 0000000..d8a0dc1 --- /dev/null +++ b/ImpLab/Debugger/AGENTS.md @@ -0,0 +1,29 @@ +# Debugger AGENTS + +## Scope +Applies to work under `ImpLab/Debugger/*`, `app/ToyDap.lean`, `app/ExportMain.lean`, and debugger-focused tests. + +## Source of truth +- Debugger behavior: `ImpLab/Debugger/Core.lean` +- Session semantics: `ImpLab/Debugger/Session.lean` +- DAP transport: `ImpLab/Debugger/DAP/Stdio.lean` +- Widget transport: `ImpLab/Debugger/Widget/Server.lean` + +## Rules +- Put new debugger behavior in `Core.lean` first, then wire transports. +- Keep transport files as adapters only; avoid protocol/state duplication. +- Treat `ProgramInfo` as canonical across launch/debug/export flows. +- Keep source mapping coherent (function + statement line <-> source line). +- Preserve stable DAP JSON payload shapes. + +## Testing split +- Core behavior tests: `Test/Core.lean`. +- Transport tests: `Test/Transport.lean`. +- DAP sanity must include lifecycle ordering and at least one breakpoint hit path. + +## Review checklist +- Is behavior duplicated in `Widget/Server.lean` or `DAP/Stdio.lean` that belongs in core? +- Any hardcoded entrypoint/decl list that should be generalized? +- Any duplicated decode/source-mapping logic that can drift? +- Are stack and breakpoint lines mapped correctly for all functions via `ProgramInfo`? +- Are lifecycle events ordered correctly (`initialized`, `stopped`, `continued`, `terminated`)? diff --git a/README.md b/README.md index 4a72f71..4ad75ea 100644 --- a/README.md +++ b/README.md @@ -1,61 +1,36 @@ # imp-lab -Lean 4 toy debugger project with: -- a small function-based toy language, -- a pure debugger core, -- a standalone DAP adapter (`toydap`), -- a VS Code side-load client (`client/`), -- Lean widget RPC endpoints for infoview demos. +ImpLab is a Lean playground to showcase Lean's capabilities for programming language modeling, debugging, and education. -## Beginner guide (no DAP background needed) +## What is in this repo -This project has two ways to use the debugger: -1. VS Code mode (primary): debug from VS Code using the `lean-toy-dap` extension. -2. Lean widget mode: debug inside Lean infoview via `#widget`. +- `ImpLab/Lang/*`: toy language AST, DSL, evaluator, traces. +- `ImpLab/Debugger/*`: debugger core, DAP transport, widget transport. +- `examples/Main.lean`: default `mainProgram` fixture. +- `client/`: VS Code extension for the standalone `toydap` adapter. -### VS Code quick start (recommended) - -1. Build Lean artifacts: +## Quick start ```bash lake build +lake exe dap-tests +lake exe toydap ``` -2. Install client dependencies (first time only): - -```bash -cd client && npm i -``` - -3. Start the extension dev host: +For VS Code client: ```bash -code client +cd client +npm install +npm run compile ``` -4. In that VS Code window, press `F5` and choose: -- `Run ImpLab Toy DAP Extension (watch)` (recommended), or -- `Run ImpLab Toy DAP Extension (compile once)`. - -5. In the Extension Development Host that opens: -- open this repository, -- open `examples/Main.lean`, -- run debug config `ImpLab Toy DAP (auto-export ProgramInfo)` from `.vscode/launch.json`. -- if you need to create/edit one manually, see [VS Code launch process and config](#vs-code-launch-process-and-config). - -The extension launches `toydap` automatically (default path: `${workspaceFolder}/.lake/build/bin/toydap`). - -By default, it will debug the program named `mainProgram`; see [VS Code launch process and config](#vs-code-launch-process-and-config) for how to customize this. - -### Lean widget quick start - -In a Lean file: +## Minimal Lean example ```lean import Lean import ImpLab.Debugger.Widget.UI import ImpLab.Debugger.Widget.Server -import ImpLab.Debugger.Widget.Types import ImpLab.Lang.Dsl open ImpLab @@ -72,162 +47,20 @@ def mainProgram : ProgramInfo := dap%[ } ] -def mainProps : TraceWidgetInitProps := +def props : TraceWidgetInitProps := { programInfo := mainProgram, stopOnEntry := true } -#widget ImpLab.traceExplorerWidget with Lean.toJson mainProps +#widget ImpLab.traceExplorerWidget with Lean.toJson props ``` -The widget launches a live debugger session and shows grouped function code, current function/pc/source location, call stack, and locals while stepping. - -### Toy language reference - -The language has one term elaborator: -- `dap%[...] : ImpLab.ProgramInfo` - -`dap%[...]` accepts only function definitions and must include `main()` as entrypoint. - -Statements: - -```lean -let v := N -let v := add v1 v2 -let v := sub v1 v2 -let v := mul v1 v2 -let v := div v1 v2 -let v := call f(a, b, ...) -return v -``` - -Example: - -```lean -def p : ImpLab.ProgramInfo := dap%[ - def addMul(x, y) := { - let s := add x y, - let z := mul s y, - return z - }, - def main() := { - let a := 2, - let b := 5, - let out := call addMul(a, b) - } -] -``` - -`ProgramInfo.located` stores source locations with function context (`func`, `stmtLine`, `span`), which powers function-aware breakpoints and stack traces. - -## Internals and advanced configuration - -### VS Code launch process and config - -A launch config is a VS Code debug profile (JSON in `launch.json`) that tells VS Code: -- which debugger type to run (`lean-toy-dap`), -- how to launch it (`request: launch`), -- which inputs to pass (`programInfo`, `source`, `stopOnEntry`, etc.). +## Documentation -Launch flow in this repository: -1. You run `ImpLab Toy DAP (auto-export ProgramInfo)` from `.vscode/launch.json`. -2. Its `preLaunchTask` runs `dap-export` and writes `.dap/programInfo.generated.json`. -3. The extension launches `toydap`. -4. If `programInfo` is not inline in launch JSON, the extension auto-loads `.dap/programInfo.generated.json`. +- Debugger architecture, DAP flow, launch configuration, and transport details: + - `docs/debugger.md` +- VS Code extension details: + - `client/README.md` -Minimal config (customize as needed): +## Naming notes -```json -{ - "name": "ImpLab Toy DAP", - "type": "lean-toy-dap", - "request": "launch", - "source": "${file}", - "stopOnEntry": true -} -``` - -Notes: -- `programInfo` is required to launch. -- With the provided auto-export launch setup, you usually do not need to set `programInfo` manually. -- Launch fails if neither inline `programInfo` nor valid `.dap/programInfo.generated.json` is available. -- `source` is optional and controls displayed source path in stack frames. -- `toydapPath` (optional, `string`): explicit adapter binary path. -- If `toydapPath` is omitted, the extension tries `${workspaceFolder}/.lake/build/bin/toydap`, then `toydap` from `PATH`. -- `toydapArgs` (optional, `string[]`): extra arguments passed to the `toydap` process. - -Manual export (advanced/internal): generate source-aware JSON from a Lean declaration: - -```bash -lake exe dap-export --decl ImpLab.Lang.Examples.mainProgram --out .dap/programInfo.generated.json -``` - -Using a different declaration than `mainProgram`: - -```bash -lake exe dap-export --decl MyProject.Debugger.lesson1Program --out .dap/programInfo.generated.json -``` - -Then launch normally from VS Code; the extension will pick up the newly generated `.dap/programInfo.generated.json`. - -`--decl` must resolve to an `ImpLab.ProgramInfo` declaration. - -`toydap` CLI arguments (`lake exe toydap --help`): -- No CLI flags are currently supported. -- `toydap` runs as a stdio DAP server and expects DAP messages on stdin. - -### VS Code side-load client - -The `client/` extension launches `toydap`. - -See `client/README.md` for packaging/sideload options and full launch details. - -### Execution model - -The interpreter uses explicit call frames: -- each frame has function name, local environment, and program counter, -- `call` pushes a frame, -- `return` pops and assigns into caller destination, -- stepping (`step`) is the semantic foundation for runtime and debugger behavior. - -### Lean RPC widget methods - -Registered in `ImpLab.Debugger.Widget.Server`: -- `ImpLab.Debugger.Widget.Server.widgetLaunch` -- `ImpLab.Debugger.Widget.Server.widgetStepIn` -- `ImpLab.Debugger.Widget.Server.widgetStepBack` -- `ImpLab.Debugger.Widget.Server.widgetContinue` -- `ImpLab.Debugger.Widget.Server.widgetDisconnect` - -`widgetLaunch` accepts `programInfo` plus optional `stopOnEntry` and `breakpoints`. - -### Project layout - -- `app/` executables: - - `app/ToyDap.lean`: stdio DAP adapter entrypoint (`lake exe toydap`). - - `app/ExportMain.lean`: `ProgramInfo` export CLI (`lake exe dap-export`). - - These files are intentional thin entrypoints; logic lives under `ImpLab/*`. -- `ImpLab/Lang/Ast.lean`: core AST (`Program` is a list of functions, entrypoint is `main`). -- `ImpLab/Lang/Dsl.lean`: DSL syntax/macros (`dap%[...]`) + infotree metadata. -- `ImpLab/Lang/Eval.lean`: environment, call-stack semantics, small-step transition, and full runner. -- `ImpLab/Lang/History.lean`: shared cursor/history navigation helpers. -- `ImpLab/Lang/Trace.lean`: execution trace and navigation API (`Explorer`). -- `examples/Main.lean`: sample program and widget launch props. -- `ImpLab/Debugger/Session.lean`: pure debugger session model (breakpoints, continue, next, stepIn, stepOut, stepBack). -- `ImpLab/Debugger/Core.lean`: session store + DAP-shaped pure core operations. -- `ImpLab/Debugger/Widget/Server.lean`: Lean server RPC endpoints implementing DAP-like operations. -- `ImpLab/Debugger/DAP/Stdio.lean`: standalone DAP adapter implementation (native DAP protocol over stdio). -- `ImpLab/Debugger/Widget/Types.lean`: widget launch/session view models and session-to-widget projection helpers. -- `ImpLab/Debugger/Widget/UI.lean`: `traceExplorerWidget` module UI. -- `ImpLab/Debugger/DAP/Export.lean`: `dap-export` declaration loader/export logic. -- `Test/Core.lean`: core/runtime/debugger tests. -- `Test/Transport.lean`: DAP stdio transport lifecycle/framing tests. -- `Test/Main.lean`: test runner executable. -- `client/`: VS Code extension scaffold for side-loading (`lean-toy-dap` debug type). - -### Dev commands - -```bash -lake build -lake exe toydap -lake exe dap-export --help -lake exe dap-tests -``` +- The project is `imp-lab` / `ImpLab`. +- DAP protocol-specific names intentionally remain where appropriate (`toydap`, `dap-export`, `dap-tests`, `lean-toy-dap`, `.dap/`). diff --git a/docs/debugger.md b/docs/debugger.md new file mode 100644 index 0000000..cb27675 --- /dev/null +++ b/docs/debugger.md @@ -0,0 +1,80 @@ +# Debugger + +This document contains debugger-specific architecture, launch flow, and protocol details. + +## Components + +- Core semantics: + - `ImpLab/Debugger/Core.lean` + - `ImpLab/Debugger/Session.lean` +- StdIO DAP transport: + - `ImpLab/Debugger/DAP/Stdio.lean` + - `app/ToyDap.lean` +- Lean widget transport: + - `ImpLab/Debugger/Widget/Server.lean` + - `ImpLab/Debugger/Widget/UI.lean` + - `ImpLab/Debugger/Widget/Types.lean` +- ProgramInfo loading/export: + - `ImpLab/Debugger/DAP/ProgramInfoLoader.lean` + - `ImpLab/Debugger/DAP/Export.lean` + - `app/ExportMain.lean` + +## Architecture guardrails + +- Put debugger behavior in `ImpLab/Debugger/Core.lean` first. +- Keep transport files as adapters only. +- Treat `ProgramInfo` as canonical across launch/debug/export. +- Keep source mapping coherent (`func` + `stmtLine` <-> source line). +- Preserve DAP payload shape stability and lifecycle ordering. + +## VS Code launch flow + +1. Run `ImpLab Toy DAP (auto-export ProgramInfo)` from `.vscode/launch.json`. +2. `preLaunchTask` runs `dap-export` to write `.dap/programInfo.generated.json`. +3. Extension launches `toydap` (`.lake/build/bin/toydap` by default). +4. If `programInfo` is missing inline, extension loads `.dap/programInfo.generated.json`. + +Minimal launch config: + +```json +{ + "name": "ImpLab Toy DAP", + "type": "lean-toy-dap", + "request": "launch", + "source": "${file}", + "stopOnEntry": true +} +``` + +## Launch contract + +- `programInfo` is required at launch. +- `source` is optional and affects source display in stack frames. +- `toydapPath` and `toydapArgs` are optional adapter controls. + +Export example: + +```bash +lake exe dap-export --decl ImpLab.Lang.Examples.mainProgram --out .dap/programInfo.generated.json +``` + +`--decl` must resolve to an `ImpLab.ProgramInfo` declaration. + +## Lifecycle and behavior checks + +- Event order must remain coherent (`initialized`, `stopped`, `continued`, `terminated`). +- Breakpoint verification and stack-frame/source mapping must remain function-aware. +- `Program` stays function-only with required `main()`. + +## Tests + +```bash +lake build +lake exe dap-tests +cd client && npm run compile +``` + +Key tests: + +- `Test/Core.lean`: core behavior and debugger semantics. +- `Test/Transport.lean`: stdio framing, request wiring, lifecycle and breakpoint sanity. From aa33e94f76bae8e9bc59386d477681c69a4a4954 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 24 Feb 2026 21:59:58 +0100 Subject: [PATCH 3/9] Restore missing docs after README split --- README.md | 2 ++ docs/debugger.md | 56 ++++++++++++++++++++++++++++++++++++++++++++---- docs/language.md | 43 +++++++++++++++++++++++++++++++++++++ 3 files changed, 97 insertions(+), 4 deletions(-) create mode 100644 docs/language.md diff --git a/README.md b/README.md index 4ad75ea..aaf3b0e 100644 --- a/README.md +++ b/README.md @@ -55,6 +55,8 @@ def props : TraceWidgetInitProps := ## Documentation +- Language DSL and semantics reference: + - `docs/language.md` - Debugger architecture, DAP flow, launch configuration, and transport details: - `docs/debugger.md` - VS Code extension details: diff --git a/docs/debugger.md b/docs/debugger.md index cb27675..e657211 100644 --- a/docs/debugger.md +++ b/docs/debugger.md @@ -14,8 +14,7 @@ This document contains debugger-specific architecture, launch flow, and protocol - `ImpLab/Debugger/Widget/Server.lean` - `ImpLab/Debugger/Widget/UI.lean` - `ImpLab/Debugger/Widget/Types.lean` -- ProgramInfo loading/export: - - `ImpLab/Debugger/DAP/ProgramInfoLoader.lean` +- ProgramInfo export: - `ImpLab/Debugger/DAP/Export.lean` - `app/ExportMain.lean` @@ -27,6 +26,35 @@ This document contains debugger-specific architecture, launch flow, and protocol - Keep source mapping coherent (`func` + `stmtLine` <-> source line). - Preserve DAP payload shape stability and lifecycle ordering. +## VS Code quick start + +1. Build Lean artifacts: + +```bash +lake build +``` + +2. Install client dependencies (first time only): + +```bash +cd client && npm i +``` + +3. Start the extension dev host: + +```bash +code client +``` + +4. In that VS Code window, press `F5` and run one of: +- `Run ImpLab Toy DAP Extension (watch)` +- `Run ImpLab Toy DAP Extension (compile once)` + +5. In the Extension Development Host: +- open this repository, +- open `examples/Main.lean`, +- run `ImpLab Toy DAP (auto-export ProgramInfo)` from `.vscode/launch.json`. + ## VS Code launch flow 1. Run `ImpLab Toy DAP (auto-export ProgramInfo)` from `.vscode/launch.json`. @@ -49,17 +77,38 @@ Minimal launch config: ## Launch contract - `programInfo` is required at launch. +- Launch fails if neither inline `programInfo` nor valid `.dap/programInfo.generated.json` is available. - `source` is optional and affects source display in stack frames. - `toydapPath` and `toydapArgs` are optional adapter controls. -Export example: +Export examples: ```bash lake exe dap-export --decl ImpLab.Lang.Examples.mainProgram --out .dap/programInfo.generated.json +lake exe dap-export --decl MyProject.Debugger.lesson1Program --out .dap/programInfo.generated.json ``` `--decl` must resolve to an `ImpLab.ProgramInfo` declaration. +## Execution model + +The interpreter uses explicit call frames: +- each frame has function name, local environment, and program counter, +- `call` pushes a frame, +- `return` pops and assigns into caller destination, +- stepping (`step`) is the semantic foundation for runtime and debugger behavior. + +## Widget RPC methods + +Registered in `ImpLab.Debugger.Widget.Server`: +- `ImpLab.Debugger.Widget.Server.widgetLaunch` +- `ImpLab.Debugger.Widget.Server.widgetStepIn` +- `ImpLab.Debugger.Widget.Server.widgetStepBack` +- `ImpLab.Debugger.Widget.Server.widgetContinue` +- `ImpLab.Debugger.Widget.Server.widgetDisconnect` + +`widgetLaunch` accepts `programInfo` plus optional `stopOnEntry` and `breakpoints`. + ## Lifecycle and behavior checks - Event order must remain coherent (`initialized`, `stopped`, `continued`, `terminated`). @@ -75,6 +124,5 @@ cd client && npm run compile ``` Key tests: - - `Test/Core.lean`: core behavior and debugger semantics. - `Test/Transport.lean`: stdio framing, request wiring, lifecycle and breakpoint sanity. diff --git a/docs/language.md b/docs/language.md new file mode 100644 index 0000000..9668845 --- /dev/null +++ b/docs/language.md @@ -0,0 +1,43 @@ +# Language + +ImpLab includes a small function-based toy language designed for interpreter and debugger experiments. + +## DSL entrypoint + +- `dap%[...] : ImpLab.ProgramInfo` +- `dap%[...]` accepts only function definitions. +- A `main()` function (zero params) is required. + +## Statements + +```lean +let v := N +let v := add v1 v2 +let v := sub v1 v2 +let v := mul v1 v2 +let v := div v1 v2 +let v := call f(a, b, ...) +return v +``` + +## Example + +```lean +def p : ImpLab.ProgramInfo := dap%[ + def addMul(x, y) := { + let s := add x y, + let z := mul s y, + return z + }, + def main() := { + let a := 2, + let b := 5, + let out := call addMul(a, b) + } +] +``` + +## Source mapping + +`ProgramInfo.located` stores source locations with function context (`func`, `stmtLine`, `span`). +This powers function-aware breakpoints and stack traces. From 18f922f7c0115da4a065a364a3f170e17c169fb6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 24 Feb 2026 22:02:09 +0100 Subject: [PATCH 4/9] Rewrite README for human-first debugger onboarding --- README.md | 91 +++++++++++++++++++++++++++---------------------------- 1 file changed, 44 insertions(+), 47 deletions(-) diff --git a/README.md b/README.md index aaf3b0e..38d1fb2 100644 --- a/README.md +++ b/README.md @@ -1,68 +1,65 @@ # imp-lab -ImpLab is a Lean playground to showcase Lean's capabilities for programming language modeling, debugging, and education. +ImpLab is a Lean playground for programming language modeling and teaching-oriented tooling. -## What is in this repo +Today the core feature is the debugger, available in two modes: as a [Debug Adapter Protocol (DAP)](https://microsoft.github.io/debug-adapter-protocol/) server (`toydap`) for editor integration, and as an in-editor Lean UI built with [ProofWidgets](https://github.com/leanprover-community/ProofWidgets4). -- `ImpLab/Lang/*`: toy language AST, DSL, evaluator, traces. -- `ImpLab/Debugger/*`: debugger core, DAP transport, widget transport. -- `examples/Main.lean`: default `mainProgram` fixture. -- `client/`: VS Code extension for the standalone `toydap` adapter. +## Run the debugger -## Quick start +### 1) Build everything once ```bash lake build -lake exe dap-tests -lake exe toydap +cd client && npm install && npm run compile ``` -For VS Code client: +### 2) Run in VS Code (DAP mode) + +1. Open the extension project: ```bash -cd client -npm install -npm run compile +code client ``` -## Minimal Lean example +2. In that VS Code window, press `F5` and run one of: +- `Run ImpLab Toy DAP Extension (watch)` +- `Run ImpLab Toy DAP Extension (compile once)` + +3. In the Extension Development Host window: +- open this repository, +- open `examples/Main.lean`, +- run debug config `ImpLab Toy DAP (auto-export ProgramInfo)`. + +Notes: +- The launch config auto-generates `.dap/programInfo.generated.json` using `dap-export`. +- The adapter binary is `toydap`. + +### 3) Run in Lean (ProofWidgets mode) + +1. Open `examples/Main.lean`. +2. Ensure the Lean infoview is active. +3. Evaluate the widget declaration at the end of the file: ```lean -import Lean -import ImpLab.Debugger.Widget.UI -import ImpLab.Debugger.Widget.Server -import ImpLab.Lang.Dsl - -open ImpLab - -def mainProgram : ProgramInfo := dap%[ - def inc(x) := { - let one := 1, - let out := add x one, - return out - }, - def main() := { - let seed := 5, - let out := call inc(seed) - } -] - -def props : TraceWidgetInitProps := - { programInfo := mainProgram, stopOnEntry := true } - -#widget ImpLab.traceExplorerWidget with Lean.toJson props +#widget ImpLab.traceExplorerWidget with ImpLab.Lang.Examples.sampleTracePropsJson ``` -## Documentation +This launches a debugger session directly in infoview. + +## Language + +ImpLab includes a small function-based toy language with a dedicated DSL elaborator: + +- `dap%[...] : ImpLab.ProgramInfo` +- function-only definitions +- required `main()` entrypoint -- Language DSL and semantics reference: - - `docs/language.md` -- Debugger architecture, DAP flow, launch configuration, and transport details: - - `docs/debugger.md` -- VS Code extension details: - - `client/README.md` +Language reference and examples: +- `docs/language.md` -## Naming notes +## Additional links -- The project is `imp-lab` / `ImpLab`. -- DAP protocol-specific names intentionally remain where appropriate (`toydap`, `dap-export`, `dap-tests`, `lean-toy-dap`, `.dap/`). +- Debugger architecture and launch contract: `docs/debugger.md` +- VS Code extension details: `client/README.md` +- Agent instructions (global): `AGENTS.md` +- Agent instructions (debugger-local): `ImpLab/Debugger/AGENTS.md` From 339714aaf5e5bf34a54f1db0f467fe2ccaf5ac6c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 24 Feb 2026 22:09:38 +0100 Subject: [PATCH 5/9] Rename DSL elaborator to imp% and refresh language docs --- AGENTS.md | 4 +-- ImpLab/Lang/Dsl.lean | 62 ++++++++++++++++++++--------------------- README.md | 31 +++++++++++++++++---- Test/Core.lean | 24 ++++++++-------- client/README.md | 2 +- client/src/extension.ts | 2 +- docs/language.md | 6 ++-- examples/Main.lean | 2 +- 8 files changed, 77 insertions(+), 56 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index 8337762..1abdfda 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -20,8 +20,8 @@ - `cd client && npm run compile` ## Global conventions -- `dap%[...]` is the only DSL elaborator and must produce `ProgramInfo`. -- `dap%[...]` accepts functions only and must include `main()` (zero params). +- `imp%[...]` is the only DSL elaborator and must produce `ProgramInfo`. +- `imp%[...]` accepts functions only and must include `main()` (zero params). - Keep `mainProgram` as default fixture entrypoint in `examples/Main.lean`. - Prefer `initialize` over `builtin_initialize` in project code. diff --git a/ImpLab/Lang/Dsl.lean b/ImpLab/Lang/Dsl.lean index d6bf1b4..2aa38ca 100644 --- a/ImpLab/Lang/Dsl.lean +++ b/ImpLab/Lang/Dsl.lean @@ -13,44 +13,44 @@ open Lean.Elab.Term namespace ImpLab -declare_syntax_cat dap_rhs -declare_syntax_cat dap_stmt -declare_syntax_cat dap_func +declare_syntax_cat imp_rhs +declare_syntax_cat imp_stmt +declare_syntax_cat imp_func -syntax num : dap_rhs -syntax "-" num : dap_rhs -syntax "add" ident ident : dap_rhs -syntax "sub" ident ident : dap_rhs -syntax "mul" ident ident : dap_rhs -syntax "div" ident ident : dap_rhs -syntax "call" ident "(" ident,* ")" : dap_rhs +syntax num : imp_rhs +syntax "-" num : imp_rhs +syntax "add" ident ident : imp_rhs +syntax "sub" ident ident : imp_rhs +syntax "mul" ident ident : imp_rhs +syntax "div" ident ident : imp_rhs +syntax "call" ident "(" ident,* ")" : imp_rhs -syntax "let " ident " := " dap_rhs : dap_stmt -syntax "return " ident : dap_stmt +syntax "let " ident " := " imp_rhs : imp_stmt +syntax "return " ident : imp_stmt -syntax "def " ident "(" ident,* ")" " := " "{" dap_stmt,* "}" : dap_func +syntax "def " ident "(" ident,* ")" " := " "{" imp_stmt,* "}" : imp_func /-- Program literal syntax for the toy language. -`dap%[...]` must contain only function definitions and include `main()` as entrypoint. +`imp%[...]` must contain only function definitions and include `main()` as entrypoint. -/ -syntax (name := dapProgramTerm) "dap%[" dap_func,* "]" : term +syntax (name := impProgramTerm) "imp%[" imp_func,* "]" : term /-- Convenience command macro to define a program declaration from DSL syntax. -The declaration type is inferred from the right-hand side (`ProgramInfo` for `dap%[...]`). +The declaration type is inferred from the right-hand side (`ProgramInfo` for `imp%[...]`). -/ -syntax (name := dapProgramDefCmd) "dap_program " ident " := " term : command +syntax (name := impProgramDefCmd) "imp_program " ident " := " term : command macro_rules - | `(dap_program $name:ident := $program:term) => + | `(imp_program $name:ident := $program:term) => `(def $name := $program) private structure ProgramSyntaxInfo where located : Array LocatedStmt deriving TypeName -/-- Convert the custom infotree payload generated by `dap%[...]`. -/ +/-- Convert the custom infotree payload generated by `imp%[...]`. -/ def getProgramSyntaxInfo? : Elab.Info → Option (Array LocatedStmt) | .ofCustomInfo custom => (custom.value.get? ProgramSyntaxInfo).map (·.located) @@ -68,27 +68,27 @@ private def parseNatLiteral (numStx : TSyntax `num) : TermElabM Nat := throwErrorAt numStx "expected a natural number literal" private def parseRhs : Syntax → TermElabM Rhs - | `(dap_rhs| $n:num) => do + | `(imp_rhs| $n:num) => do pure (.const (Int.ofNat (← parseNatLiteral n))) - | `(dap_rhs| - $n:num) => do + | `(imp_rhs| - $n:num) => do pure (.const (-(Int.ofNat (← parseNatLiteral n)))) - | `(dap_rhs| add $lhs:ident $rhs:ident) => + | `(imp_rhs| add $lhs:ident $rhs:ident) => pure (.bin .add (varOfIdent lhs) (varOfIdent rhs)) - | `(dap_rhs| sub $lhs:ident $rhs:ident) => + | `(imp_rhs| sub $lhs:ident $rhs:ident) => pure (.bin .sub (varOfIdent lhs) (varOfIdent rhs)) - | `(dap_rhs| mul $lhs:ident $rhs:ident) => + | `(imp_rhs| mul $lhs:ident $rhs:ident) => pure (.bin .mul (varOfIdent lhs) (varOfIdent rhs)) - | `(dap_rhs| div $lhs:ident $rhs:ident) => + | `(imp_rhs| div $lhs:ident $rhs:ident) => pure (.bin .div (varOfIdent lhs) (varOfIdent rhs)) - | `(dap_rhs| call $fn:ident($args:ident,*)) => + | `(imp_rhs| call $fn:ident($args:ident,*)) => pure (.call (varOfIdent fn) (args.getElems.map varOfIdent)) | stx => throwErrorAt stx "invalid right-hand side" private def parseStmt : Syntax → TermElabM Stmt - | `(dap_stmt| let $dest:ident := $rhs:dap_rhs) => do + | `(imp_stmt| let $dest:ident := $rhs:imp_rhs) => do pure (.assign (varOfIdent dest) (← parseRhs rhs)) - | `(dap_stmt| return $value:ident) => + | `(imp_stmt| return $value:ident) => pure (.return_ (varOfIdent value)) | stx => throwErrorAt stx @@ -118,7 +118,7 @@ private structure ParsedFunc where located : Array LocatedStmt private def parseFunc : FileMap → Syntax → TermElabM ParsedFunc - | fileMap, `(dap_func| def $name:ident($params:ident,*) := { $body:dap_stmt,* }) => do + | fileMap, `(imp_func| def $name:ident($params:ident,*) := { $body:imp_stmt,* }) => do let bodyStx := body.getElems let bodyStmt ← bodyStx.mapM parseStmt let mut located : Array LocatedStmt := #[] @@ -159,8 +159,8 @@ private def validateFunctionSet (funcs : Array FuncDef) : TermElabM Unit := do if hasDup then throwError "Invalid DSL program: duplicate function names are not allowed." -@[term_elab dapProgramTerm] -def elabDapProgram : TermElab := fun stx _expectedType? => withRef stx do +@[term_elab impProgramTerm] +def elabImpProgram : TermElab := fun stx _expectedType? => withRef stx do let fileMap ← getFileMap let funcStx := stx[1].getSepArgs let parsed ← funcStx.mapM (parseFunc fileMap) diff --git a/README.md b/README.md index 38d1fb2..6ab7aa8 100644 --- a/README.md +++ b/README.md @@ -48,13 +48,34 @@ This launches a debugger session directly in infoview. ## Language -ImpLab includes a small function-based toy language with a dedicated DSL elaborator: +ImpLab includes a small imperative language with: -- `dap%[...] : ImpLab.ProgramInfo` -- function-only definitions -- required `main()` entrypoint +- integer literals and local variables, +- arithmetic operations (`add`, `sub`, `mul`, `div`), +- function calls with parameters, +- source-aware program metadata used by the debugger. -Language reference and examples: +Programs are written with: + +- `imp%[...] : ImpLab.ProgramInfo` + +Example: + +```lean +def sample : ImpLab.ProgramInfo := imp%[ + def inc(x) := { + let one := 1, + let out := add x one, + return out + }, + def main() := { + let seed := 5, + let out := call inc(seed) + } +] +``` + +Language reference: - `docs/language.md` ## Additional links diff --git a/Test/Core.lean b/Test/Core.lean index 608aa6c..8876f60 100644 --- a/Test/Core.lean +++ b/Test/Core.lean @@ -193,7 +193,7 @@ def testWidgetProps : IO Unit := do assertEq "widget initial function" props.state.functionName Program.mainName def testWidgetSessionProjectionAfterStep : IO Unit := do - let info : ProgramInfo := dap%[ + let info : ProgramInfo := imp%[ def main() := { let x := 2, let y := 8, @@ -209,7 +209,7 @@ def testWidgetSessionProjectionAfterStep : IO Unit := do assertEq "widget step state stmt line" props.state.stmtLine 2 def testStepBackAfterTermination : IO Unit := do - let info : ProgramInfo := dap%[ + let info : ProgramInfo := imp%[ def main() := { let x := 1 } @@ -223,7 +223,7 @@ def testStepBackAfterTermination : IO Unit := do assertEq "stepBack term cursor rewound" data.session.currentPc 0 def testWidgetInitProps : IO Unit := do - let info : ProgramInfo := dap%[ + let info : ProgramInfo := imp%[ def main() := { let x := 1 } @@ -308,7 +308,7 @@ def testDebugSessionStepBack : IO Unit := do assertEq "stepBack replay current pc" replayed.currentPc forwarded.currentPc def testDebugCoreStepInOut : IO Unit := do - let info : ProgramInfo := dap%[ + let info : ProgramInfo := imp%[ def inner(x) := { let two := 2, let out := mul x two, @@ -359,7 +359,7 @@ def testDebugCoreStepInOut : IO Unit := do assertEq "step in/out return from main terminated" outMain.terminated true def testDebugCoreNextStepsOverCall : IO Unit := do - let info : ProgramInfo := dap%[ + let info : ProgramInfo := imp%[ def double(x) := { let two := 2, let out := mul x two, @@ -386,7 +386,7 @@ def testDebugCoreNextStepsOverCall : IO Unit := do (vars.variables.any fun v => v.name == "b" && v.value == "8") def testDslProgram : IO Unit := do - let info : ProgramInfo := dap%[ + let info : ProgramInfo := imp%[ def main() := { let x := 6, let y := 7, @@ -400,7 +400,7 @@ def testDslProgram : IO Unit := do assertSomeEq "dsl result" (ctx.lookup? "z") 13 def testDslNegativeLiteral : IO Unit := do - let info : ProgramInfo := dap%[ + let info : ProgramInfo := imp%[ def main() := { let x := -6, let y := 2, @@ -414,7 +414,7 @@ def testDslNegativeLiteral : IO Unit := do assertSomeEq "dsl negative literal result" (ctx.lookup? "z") (-4) def testDslFunctionCall : IO Unit := do - let info : ProgramInfo := dap%[ + let info : ProgramInfo := imp%[ def addMul(x, y) := { let sum := add x y, let out := mul sum y, @@ -433,7 +433,7 @@ def testDslFunctionCall : IO Unit := do assertSomeEq "dsl function call result" (ctx.lookup? "z") 35 def testDslProgramInfo : IO Unit := do - let info : ProgramInfo := dap%[ + let info : ProgramInfo := imp%[ def main() := { let a := 1, let b := 2, @@ -471,7 +471,7 @@ def testProgramInfoValidation : IO Unit := do assertTrue "programInfo mismatch error mentions located size" (err.contains "located") def testDebugCoreFlow : IO Unit := do - let info : ProgramInfo := dap%[ + let info : ProgramInfo := imp%[ def main() := { let x := 5, let y := 7, @@ -500,7 +500,7 @@ def testDebugCoreFlow : IO Unit := do pure () def testDebugCoreStackFrames : IO Unit := do - let info : ProgramInfo := dap%[ + let info : ProgramInfo := imp%[ def addMul(x, y) := { let sum := add x y, let out := mul sum y, @@ -535,7 +535,7 @@ def testDebugCoreStackFrames : IO Unit := do (varsCaller.variables.any fun v => v.name == "a" && v.value == "2") def testDebugCoreTerminatedGuards : IO Unit := do - let info : ProgramInfo := dap%[ + let info : ProgramInfo := imp%[ def main() := { let x := 1 } diff --git a/client/README.md b/client/README.md index 27881fd..d151a40 100644 --- a/client/README.md +++ b/client/README.md @@ -58,7 +58,7 @@ For JSON payload shape, see `client/programInfo.sample.json`. You can also generate `ProgramInfo` JSON via: ```bash -lake exe dap-export --decl mainProgram --out .dap/programInfo.generated.json +lake exe dap-export --decl ImpLab.Lang.Examples.mainProgram --out .dap/programInfo.generated.json ``` ## Supported DAP requests diff --git a/client/src/extension.ts b/client/src/extension.ts index ec0a7ee..6657e58 100644 --- a/client/src/extension.ts +++ b/client/src/extension.ts @@ -88,7 +88,7 @@ class LeanToyDebugConfigurationProvider implements vscode.DebugConfigurationProv } if (!config.programInfo) { vscode.window.showErrorMessage( - "lean-toy-dap launch requires 'programInfo'. Run `lake exe dap-export --decl mainProgram --out .dap/programInfo.generated.json` or set launch.programInfo.", + "lean-toy-dap launch requires 'programInfo'. Run `lake exe dap-export --decl ImpLab.Lang.Examples.mainProgram --out .dap/programInfo.generated.json` or set launch.programInfo.", ) return null } diff --git a/docs/language.md b/docs/language.md index 9668845..2adfa9b 100644 --- a/docs/language.md +++ b/docs/language.md @@ -4,8 +4,8 @@ ImpLab includes a small function-based toy language designed for interpreter and ## DSL entrypoint -- `dap%[...] : ImpLab.ProgramInfo` -- `dap%[...]` accepts only function definitions. +- `imp%[...] : ImpLab.ProgramInfo` +- A program is written as a list of function declarations (`def name(params) := { ... }`). - A `main()` function (zero params) is required. ## Statements @@ -23,7 +23,7 @@ return v ## Example ```lean -def p : ImpLab.ProgramInfo := dap%[ +def p : ImpLab.ProgramInfo := imp%[ def addMul(x, y) := { let s := add x y, let z := mul s y, diff --git a/examples/Main.lean b/examples/Main.lean index 1a50a9d..3f8dcfe 100644 --- a/examples/Main.lean +++ b/examples/Main.lean @@ -12,7 +12,7 @@ namespace ImpLab.Lang.Examples open ImpLab -def mainProgram : ProgramInfo := dap%[ +def mainProgram : ProgramInfo := imp%[ def bump(x) := { let one := 1, let out := add x one, From c36fb397180254cc3ec985ff7e5c300d6b9b85e0 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 24 Feb 2026 22:16:48 +0100 Subject: [PATCH 6/9] Move DAP plan to debugger roadmap and deduplicate docs --- AGENTS.md | 2 ++ DAP_PLAN.md | 23 ----------------------- ImpLab/Debugger/AGENTS.md | 1 + README.md | 1 + docs/debugger-roadmap.md | 28 ++++++++++++++++++++++++++++ docs/debugger.md | 5 +++++ 6 files changed, 37 insertions(+), 23 deletions(-) delete mode 100644 DAP_PLAN.md create mode 100644 docs/debugger-roadmap.md diff --git a/AGENTS.md b/AGENTS.md index 1abdfda..b560390 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -28,3 +28,5 @@ ## Subsystem-local instructions - Debugger-specific rules and review checklist live in: - `ImpLab/Debugger/AGENTS.md` +- Debugger active work tracking lives in: + - `docs/debugger-roadmap.md` diff --git a/DAP_PLAN.md b/DAP_PLAN.md deleted file mode 100644 index bf9d386..0000000 --- a/DAP_PLAN.md +++ /dev/null @@ -1,23 +0,0 @@ -# DAP Plan - -Canonical project guardrails, architecture rules, and validation commands live in `AGENTS.md`. -This file is only for current DAP-facing priorities and open work. - -## Active priorities -1. Remove any remaining duplicated behavior between `ImpLab/Debugger/Widget/Server.lean` and `ImpLab/Debugger/DAP/Stdio.lean` by lifting semantics to `ImpLab/Debugger/Core.lean`. -2. Keep line/function source mapping explicit and centralized so stack/breakpoint rendering stays consistent. -3. Preserve strict DAP lifecycle ordering and stable payload shapes for editor compatibility. -4. Keep docs/examples aligned with `ProgramInfo`-only launch/export flows and `app/` entrypoint layout. - -## Open work queue -- Audit both transports for duplicate request validation and decode helpers. -- Add/adjust transport tests for lifecycle ordering edge cases (invalid ordering, repeated terminate/disconnect). -- Verify breakpoint and stack location mapping in multi-function traces. -- Keep `client/README.md` and root `README.md` consistent with current launch input contract. -- Keep executable roots (`app/ToyDap.lean`, `app/ExportMain.lean`) as thin wrappers only. - -## Milestones -1. Transport parity audit complete (no semantic drift from core). -2. Source-mapping checks expanded for multi-frame scenarios. -3. Lifecycle sanity suite covers error ordering paths. -4. Docs trimmed to a single non-overlapping story (`AGENTS.md` rules, `DAP_PLAN.md` priorities, `README.md` usage). diff --git a/ImpLab/Debugger/AGENTS.md b/ImpLab/Debugger/AGENTS.md index d8a0dc1..886f2ce 100644 --- a/ImpLab/Debugger/AGENTS.md +++ b/ImpLab/Debugger/AGENTS.md @@ -2,6 +2,7 @@ ## Scope Applies to work under `ImpLab/Debugger/*`, `app/ToyDap.lean`, `app/ExportMain.lean`, and debugger-focused tests. +Active debugger backlog and priorities are tracked in `docs/debugger-roadmap.md`. ## Source of truth - Debugger behavior: `ImpLab/Debugger/Core.lean` diff --git a/README.md b/README.md index 6ab7aa8..a8cd186 100644 --- a/README.md +++ b/README.md @@ -81,6 +81,7 @@ Language reference: ## Additional links - Debugger architecture and launch contract: `docs/debugger.md` +- Debugger roadmap (active priorities): `docs/debugger-roadmap.md` - VS Code extension details: `client/README.md` - Agent instructions (global): `AGENTS.md` - Agent instructions (debugger-local): `ImpLab/Debugger/AGENTS.md` diff --git a/docs/debugger-roadmap.md b/docs/debugger-roadmap.md new file mode 100644 index 0000000..d6a8ace --- /dev/null +++ b/docs/debugger-roadmap.md @@ -0,0 +1,28 @@ +# Debugger Roadmap + +This file tracks active debugger work and near-term milestones. + +Stable architecture guardrails and review policy live in: +- `ImpLab/Debugger/AGENTS.md` + +## Active priorities + +1. Remove remaining duplicated behavior between `ImpLab/Debugger/Widget/Server.lean` and `ImpLab/Debugger/DAP/Stdio.lean` by lifting semantics to `ImpLab/Debugger/Core.lean`. +2. Keep line/function source mapping explicit and centralized so stack and breakpoint rendering stay consistent. +3. Preserve strict DAP lifecycle ordering and stable payload shapes for editor compatibility. +4. Keep docs/examples aligned with `ProgramInfo`-only launch/export flows and thin `app/` entrypoints. + +## Open work queue + +- Audit both transports for duplicate request validation and decode helpers. +- Add/adjust transport tests for lifecycle edge cases (invalid ordering, repeated terminate/disconnect). +- Verify breakpoint and stack location mapping in multi-function traces. +- Keep `client/README.md`, `docs/debugger.md`, and `README.md` aligned with current launch contract. +- Keep executable roots (`app/ToyDap.lean`, `app/ExportMain.lean`) as thin wrappers. + +## Milestones + +1. Transport parity audit complete (no semantic drift from core). +2. Source-mapping checks expanded for multi-frame scenarios. +3. Lifecycle sanity suite covers error-ordering paths. +4. Docs are trimmed to non-overlapping scopes (`README.md`, `docs/debugger.md`, `ImpLab/Debugger/AGENTS.md`, and this roadmap). diff --git a/docs/debugger.md b/docs/debugger.md index e657211..2f0f78c 100644 --- a/docs/debugger.md +++ b/docs/debugger.md @@ -115,6 +115,11 @@ Registered in `ImpLab.Debugger.Widget.Server`: - Breakpoint verification and stack-frame/source mapping must remain function-aware. - `Program` stays function-only with required `main()`. +## Roadmap + +Current debugger priorities and milestones: +- `docs/debugger-roadmap.md` + ## Tests ```bash From d8fd27b7f8dc3b5dff8b381ba0ee3454fced3991 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 24 Feb 2026 22:17:41 +0100 Subject: [PATCH 7/9] Trim debugger roadmap to open work and recent completions --- docs/debugger-roadmap.md | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/docs/debugger-roadmap.md b/docs/debugger-roadmap.md index d6a8ace..61569da 100644 --- a/docs/debugger-roadmap.md +++ b/docs/debugger-roadmap.md @@ -8,9 +8,8 @@ Stable architecture guardrails and review policy live in: ## Active priorities 1. Remove remaining duplicated behavior between `ImpLab/Debugger/Widget/Server.lean` and `ImpLab/Debugger/DAP/Stdio.lean` by lifting semantics to `ImpLab/Debugger/Core.lean`. -2. Keep line/function source mapping explicit and centralized so stack and breakpoint rendering stay consistent. -3. Preserve strict DAP lifecycle ordering and stable payload shapes for editor compatibility. -4. Keep docs/examples aligned with `ProgramInfo`-only launch/export flows and thin `app/` entrypoints. +2. Expand transport tests for lifecycle edge cases (invalid ordering, repeated terminate/disconnect). +3. Strengthen multi-function source mapping checks for stack and breakpoint rendering. ## Open work queue @@ -20,9 +19,12 @@ Stable architecture guardrails and review policy live in: - Keep `client/README.md`, `docs/debugger.md`, and `README.md` aligned with current launch contract. - Keep executable roots (`app/ToyDap.lean`, `app/ExportMain.lean`) as thin wrappers. -## Milestones +## Recently completed -1. Transport parity audit complete (no semantic drift from core). -2. Source-mapping checks expanded for multi-frame scenarios. -3. Lifecycle sanity suite covers error-ordering paths. -4. Docs are trimmed to non-overlapping scopes (`README.md`, `docs/debugger.md`, `ImpLab/Debugger/AGENTS.md`, and this roadmap). +- Namespace and layout rebrand to `ImpLab` with debugger split under `ImpLab/Debugger/{DAP,Widget}`. +- Documentation split by scope: + - `README.md` for user-facing onboarding. + - `docs/debugger.md` for debugger operations. + - `docs/language.md` for language reference. + - `ImpLab/Debugger/AGENTS.md` for stable debugger guardrails. +- DSL elaborator renamed to `imp%[...]`. From 08439af158e38f178818a73c27fad9aec4621e7e Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 24 Feb 2026 22:21:46 +0100 Subject: [PATCH 8/9] Refocus debugger roadmap on active priorities and actionable tasks --- docs/debugger-roadmap.md | 31 +++++++++++++++---------------- 1 file changed, 15 insertions(+), 16 deletions(-) diff --git a/docs/debugger-roadmap.md b/docs/debugger-roadmap.md index 61569da..c9d8910 100644 --- a/docs/debugger-roadmap.md +++ b/docs/debugger-roadmap.md @@ -1,6 +1,6 @@ # Debugger Roadmap -This file tracks active debugger work and near-term milestones. +This file tracks active debugger work. Stable architecture guardrails and review policy live in: - `ImpLab/Debugger/AGENTS.md` @@ -8,23 +8,22 @@ Stable architecture guardrails and review policy live in: ## Active priorities 1. Remove remaining duplicated behavior between `ImpLab/Debugger/Widget/Server.lean` and `ImpLab/Debugger/DAP/Stdio.lean` by lifting semantics to `ImpLab/Debugger/Core.lean`. +Context: both adapters still own overlapping request/validation/update patterns. 2. Expand transport tests for lifecycle edge cases (invalid ordering, repeated terminate/disconnect). +Context: current tests cover main happy paths plus selected ordering checks, but not the full invalid-ordering matrix. 3. Strengthen multi-function source mapping checks for stack and breakpoint rendering. +Context: mapping works for core scenarios, but we still need broader multi-function and cross-step coverage. ## Open work queue -- Audit both transports for duplicate request validation and decode helpers. -- Add/adjust transport tests for lifecycle edge cases (invalid ordering, repeated terminate/disconnect). -- Verify breakpoint and stack location mapping in multi-function traces. -- Keep `client/README.md`, `docs/debugger.md`, and `README.md` aligned with current launch contract. -- Keep executable roots (`app/ToyDap.lean`, `app/ExportMain.lean`) as thin wrappers. - -## Recently completed - -- Namespace and layout rebrand to `ImpLab` with debugger split under `ImpLab/Debugger/{DAP,Widget}`. -- Documentation split by scope: - - `README.md` for user-facing onboarding. - - `docs/debugger.md` for debugger operations. - - `docs/language.md` for language reference. - - `ImpLab/Debugger/AGENTS.md` for stable debugger guardrails. -- DSL elaborator renamed to `imp%[...]`. +- Transport parity audit: + - Inventory duplicated validation/dispatch helpers in `ImpLab/Debugger/DAP/Stdio.lean` and `ImpLab/Debugger/Widget/Server.lean`. + - Propose core-level helpers in `ImpLab/Debugger/Core.lean` for shared semantics. +- Lifecycle ordering test expansion (`Test/Transport.lean`): + - Add invalid-ordering cases (commands before `launch`, repeated `disconnect`, control after termination). + - Add repeated terminal-event guards (no duplicate terminal transitions). +- Source mapping matrix (`Test/Core.lean` + `Test/Transport.lean`): + - Cover breakpoints and stack traces across multiple functions/call depths. + - Confirm mapping stability across `stepIn`, `next`, `stepOut`, and `stepBack` transitions. +- Documentation sync pass: + - Keep `README.md`, `docs/debugger.md`, and `client/README.md` aligned with the same launch contract and examples. From aa5be6c80da106bf55e24965703aa394f2461bd1 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 24 Feb 2026 22:23:15 +0100 Subject: [PATCH 9/9] Sync docs with extension launch names and roadmap status --- client/.vscode/launch.json | 4 ++-- docs/debugger-roadmap.md | 2 -- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/client/.vscode/launch.json b/client/.vscode/launch.json index c89e05d..b763173 100644 --- a/client/.vscode/launch.json +++ b/client/.vscode/launch.json @@ -2,7 +2,7 @@ "version": "0.2.0", "configurations": [ { - "name": "Run Lean Toy DAP Extension (watch)", + "name": "Run ImpLab Toy DAP Extension (watch)", "type": "extensionHost", "request": "launch", "args": [ @@ -14,7 +14,7 @@ "preLaunchTask": "npm: watch" }, { - "name": "Run Lean Toy DAP Extension (compile once)", + "name": "Run ImpLab Toy DAP Extension (compile once)", "type": "extensionHost", "request": "launch", "args": [ diff --git a/docs/debugger-roadmap.md b/docs/debugger-roadmap.md index c9d8910..3947007 100644 --- a/docs/debugger-roadmap.md +++ b/docs/debugger-roadmap.md @@ -25,5 +25,3 @@ Context: mapping works for core scenarios, but we still need broader multi-funct - Source mapping matrix (`Test/Core.lean` + `Test/Transport.lean`): - Cover breakpoints and stack traces across multiple functions/call depths. - Confirm mapping stability across `stepIn`, `next`, `stepOut`, and `stepBack` transitions. -- Documentation sync pass: - - Keep `README.md`, `docs/debugger.md`, and `client/README.md` aligned with the same launch contract and examples.