Add ProgramInfo module-ref launch path (tests only, rebased)

.vscode/launch.json

@@ -14,7 +14,8 @@
       "type": "lean-toy-dap",
       "request": "launch",
       "source": "${file}",
-      "stopOnEntry": true
+      "stopOnEntry": true,
+      "preLaunchTask": "Generate ImpLab ProgramInfo"
     }
   ]
 }

ImpLab/Debugger/DAP/Export.lean

@@ -6,7 +6,7 @@ Author: Emilio J. Gallego Arias
 
 import Lean
 import ImpLab.Lang.Ast
-import ImpLab.Debugger.DAP.Resolve
+import ImpLab.Debugger.DAP.ProgramInfoLoader
 import examples.Main
 
 open Lean
@@ -53,34 +53,8 @@ private def parseArgs : CliOptions → List String → Except String CliOptions
 private def normalizeDeclName (raw : String) : String :=
   raw.trimAscii.toString
 
-private unsafe def evalProgramInfo
-    (env : Environment) (opts : Options) (decl : Name) : Except String ProgramInfo := do
-  match env.evalConstCheck ProgramInfo opts ``ImpLab.ProgramInfo decl with
-  | .ok info =>
-    info.validate
-  | .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 ImpLab.parseDeclName? rawDecl with
-    | some n => pure n
-    | none => throw <| IO.userError s!"Invalid declaration name '{rawDecl}'"
-  let env ← ImpLab.importProjectEnv
-  let opts : Options := {}
-  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 := 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
-  | .error err => throw <| IO.userError err
+  ImpLab.loadProgramInfoFromDecl rawDecl
 
 private def renderJson (programInfo : ProgramInfo) (pretty : Bool) : String :=
   let json := toJson programInfo

ImpLab/Debugger/DAP/ProgramInfoLoader.lean

@@ -0,0 +1,79 @@
+/-
+Copyright (c) 2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Emilio J. Gallego Arias
+-/
+
+import Lean
+import ImpLab.Lang.Ast
+import ImpLab.Debugger.DAP.Resolve
+
+open Lean
+
+namespace ImpLab
+
+private def initProjectSearchPath : IO Unit := do
+  let sysroot ← Lean.findSysroot
+  Lean.initSearchPath sysroot [System.FilePath.mk ".lake/build/lib/lean"]
+
+private def parseNameOrThrow (kind raw : String) : IO Name := do
+  match ImpLab.parseName? raw with
+  | some n =>
+    pure n
+  | none =>
+    throw <| IO.userError s!"Invalid {kind} name '{raw}'"
+
+private unsafe def evalProgramInfo
+    (env : Environment) (opts : Options) (decl : Name) : Except String ProgramInfo := do
+  match env.evalConstCheck ProgramInfo opts ``ImpLab.ProgramInfo decl with
+  | .ok info =>
+    info.validate
+  | .error infoErr =>
+    throw s!"Declaration '{decl}' is not ImpLab.ProgramInfo.\nProgramInfo error: {infoErr}"
+
+private def resolveDeclOrThrow
+    (env : Environment)
+    (rawDecl : String)
+    (declName : Name)
+    (moduleName? : Option Name)
+    (includeExamples : Bool) : IO Name := do
+  let candidates := ImpLab.candidateDeclNames declName moduleName? includeExamples
+  match ImpLab.resolveFirstDecl? env candidates with
+  | some n =>
+    pure n
+  | none =>
+    let attempted := ImpLab.renderCandidateDecls candidates
+    throw <| IO.userError s!"Could not resolve declaration '{rawDecl}'. Tried: {attempted}"
+
+def loadProgramInfoFromDecl
+    (rawDecl : String)
+    (moduleName? : Option Name := some `Main)
+    (includeExamples : Bool := true) : IO ProgramInfo := do
+  initProjectSearchPath
+  let declName ← parseNameOrThrow "declaration" rawDecl
+  let env ← ImpLab.importProjectEnv
+  let resolved ← resolveDeclOrThrow env rawDecl declName moduleName? includeExamples
+  let opts : Options := {}
+  match unsafe evalProgramInfo env opts resolved with
+  | .ok info =>
+    pure info
+  | .error err =>
+    throw <| IO.userError err
+
+def loadProgramInfoFromModuleDecl
+    (rawModule : String)
+    (rawDecl : String := "mainProgram")
+    (includeExamples : Bool := false) : IO ProgramInfo := do
+  initProjectSearchPath
+  let moduleName ← parseNameOrThrow "module" rawModule
+  let declName ← parseNameOrThrow "declaration" rawDecl
+  let env ← ImpLab.importEnvForModule moduleName
+  let resolved ← resolveDeclOrThrow env rawDecl declName (some moduleName) includeExamples
+  let opts : Options := {}
+  match unsafe evalProgramInfo env opts resolved with
+  | .ok info =>
+    pure info
+  | .error err =>
+    throw <| IO.userError err
+
+end ImpLab

ImpLab/Debugger/DAP/Resolve.lean

@@ -10,13 +10,16 @@ open Lean
 
 namespace ImpLab
 
-def parseDeclName? (raw : String) : Option Name :=
+def parseName? (raw : String) : Option Name :=
   let parts := raw.trimAscii.toString.splitOn "." |>.filter (· != "")
   match parts with
   | [] => none
   | _ =>
     some <| parts.foldl Name.str Name.anonymous
 
+def parseDeclName? (raw : String) : Option Name :=
+  parseName? raw
+
 def isUnqualifiedName (n : Name) : Bool :=
   match n with
   | .str .anonymous _ => true
@@ -54,9 +57,9 @@ def resolveFirstDecl? (env : Environment) (candidates : Array Name) : Option Nam
 def renderCandidateDecls (candidates : Array Name) : String :=
   String.intercalate ", " <| candidates.toList.map (fun n => s!"'{n}'")
 
-def importProjectEnv : IO Environment := do
-  let candidates : Array (Array Name) :=
-    #[#[`Main, `ImpLab], #[`Main], #[`ImpLab]]
+private def importFirstAvailableEnv
+    (candidates : Array (Array Name))
+    (errMsg : String) : IO Environment := do
   let rec go (idx : Nat) : IO Environment := do
     if h : idx < candidates.size then
       let modules := candidates[idx]
@@ -66,7 +69,24 @@ def importProjectEnv : IO Environment := do
       catch _ =>
         go (idx + 1)
     else
-      throw <| IO.userError "Could not import project modules (`Main` or `ImpLab`) to resolve declaration"
+      throw <| IO.userError errMsg
   go 0
 
+def importProjectEnv : IO Environment := do
+  importFirstAvailableEnv
+    #[#[`Main, `ImpLab], #[`Main], #[`ImpLab]]
+    "Could not import project modules (`Main` or `ImpLab`) to resolve declaration"
+
+def importEnvForModule (moduleName : Name) : IO Environment := do
+  let candidates : Array (Array Name) :=
+    if moduleName == `ImpLab then
+      #[#[`ImpLab]]
+    else if moduleName == `Main then
+      #[#[`Main, `ImpLab], #[`Main], #[`ImpLab]]
+    else
+      #[#[moduleName, `ImpLab], #[moduleName]]
+  importFirstAvailableEnv
+    candidates
+    s!"Could not import module '{moduleName}' to resolve declaration"
+
 end ImpLab

ImpLab/Debugger/DAP/Stdio.lean

@@ -9,6 +9,7 @@ import Lean.Data.Lsp.Communication
 import ImpLab.Debugger.Core
 import ImpLab.Debugger.DAP.Launch
 import ImpLab.Debugger.DAP.Capabilities
+import ImpLab.Debugger.DAP.ProgramInfoLoader
 
 open Lean
 
@@ -131,18 +132,35 @@ private def parseStringArrayField (args : Json) (field : String) : Array String
           | .ok str => acc.push str
           | .error _ => acc)
 
-private def requireProgramInfo (args : Json) : IO ProgramInfo := do
-  let programInfoJson ←
-    match (args.getObjVal? "programInfo").toOption with
+private def decodeProgramInfoRef (json : Json) : Except String (String × String) := do
+  let moduleName ← json.getObjValAs? String "module"
+  let decl := (json.getObjValAs? String "decl").toOption.getD "mainProgram"
+  pure (moduleName, decl)
+
+private def requireProgramInfoFromRef (args : Json) : IO ProgramInfo := do
+  let refJson ←
+    match (args.getObjVal? "programInfoRef").toOption with
     | some json => pure json
     | none =>
       throw <| IO.userError
-        "launch requires 'programInfo' (a ImpLab.ProgramInfo JSON payload)."
-  match ImpLab.decodeProgramInfoJson programInfoJson with
-  | .ok programInfo =>
-    pure programInfo
-  | .error err =>
-    throw <| IO.userError err
+        "launch requires 'programInfo' (a ImpLab.ProgramInfo JSON payload) or 'programInfoRef' with 'module' and optional 'decl'."
+  let (moduleName, decl) ←
+    match decodeProgramInfoRef refJson with
+    | .ok value => pure value
+    | .error err =>
+      throw <| IO.userError s!"Invalid 'programInfoRef' payload: {err}"
+  ImpLab.loadProgramInfoFromModuleDecl moduleName decl
+
+private def requireProgramInfo (args : Json) : IO ProgramInfo := do
+  match (args.getObjVal? "programInfo").toOption with
+  | some programInfoJson =>
+    match ImpLab.decodeProgramInfoJson programInfoJson with
+    | .ok programInfo =>
+      pure programInfo
+    | .error err =>
+      throw <| IO.userError err
+  | none =>
+    requireProgramInfoFromRef args
 
 private def sourceJson? (sourcePath? : Option String) : Option Json := do
   let sourcePath ← sourcePath?

Test/Transport.lean

@@ -119,6 +119,13 @@ private def launchArgsWithGlobals (stopOnEntry : Bool) : Json :=
     [ ("programInfo", toJson globalProgramInfo),
       ("stopOnEntry", toJson stopOnEntry) ]
 
+private def launchArgsFromRef (stopOnEntry : Bool) : Json :=
+  Json.mkObj
+    [ ("programInfoRef", Json.mkObj
+      [ ("module", toJson "examples.Main"),
+        ("decl", toJson "ImpLab.Lang.Examples.mainProgram") ]),
+      ("stopOnEntry", toJson stopOnEntry) ]
+
 private def bumpEntryLine : Nat :=
   transportProgramInfo.locationToSourceLine { func := "bump", stmtLine := 1 }
 
@@ -147,6 +154,33 @@ def testToyDapProtocolSanity : IO Unit := do
   assertTrue "disconnect response present"
     (stdout.contains "\"request_seq\":5" && stdout.contains "\"command\":\"disconnect\"")
 
+def testToyDapLaunchFromProgramInfoRef : IO Unit := do
+  let stdinPayload :=
+    String.intercalate ""
+      [ encodeDapRequest 1 "initialize",
+        encodeDapRequest 2 "launch" <| launchArgsFromRef true,
+        encodeDapRequest 3 "disconnect" ]
+  let stdout ← runToyDapPayload "toydap.launch.programinforef" stdinPayload
+  assertTrue "programInfoRef launch response present"
+    (stdout.contains "\"request_seq\":2" && stdout.contains "\"command\":\"launch\"")
+  if stdout.contains "\"success\":false" then
+    throw <| IO.userError s!"programInfoRef launch has an error response: {stdout}"
+
+def testToyDapLaunchFromProgramInfoRefRejectsUnknownModule : IO Unit := do
+  let stdinPayload :=
+    String.intercalate ""
+      [ encodeDapRequest 1 "initialize",
+        encodeDapRequest 2 "launch" <| Json.mkObj
+          [ ("programInfoRef", Json.mkObj
+            [ ("module", toJson "No.Such.Module"),
+              ("decl", toJson "mainProgram") ]),
+            ("stopOnEntry", toJson true) ],
+        encodeDapRequest 3 "disconnect" ]
+  let stdout ← runToyDapPayload "toydap.launch.programinforef.invalid.module" stdinPayload
+  assertTrue "invalid module launch request gets an error response"
+    (stdout.contains "\"request_seq\":2" &&
+      stdout.contains "Could not import module 'No.Such.Module'")
+
 def testToyDapBreakpointProtocol : IO Unit := do
   let stdinPayload :=
     String.intercalate ""
@@ -539,6 +573,8 @@ def testToyDapDisconnectCanTargetSessionId : IO Unit := do
 
 def runTransportTests : IO Unit := do
   testToyDapProtocolSanity
+  testToyDapLaunchFromProgramInfoRef
+  testToyDapLaunchFromProgramInfoRefRejectsUnknownModule
   testToyDapBreakpointProtocol
   testToyDapContinueEventOrder
   testToyDapStepInOutProtocol

client/README.md

@@ -33,6 +33,7 @@ Launch 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.
+- Launch data comes from compiled `.olean` artifacts (via export), so unsaved or unbuilt Lean changes are not reflected.
 
 Adapter executable:
 - `toydapPath` (optional): explicit path to the `toydap` binary.

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.29.0-rc1
+leanprover/lean4:v4.29.0