From 65a0c618068bd01a933596cdb6dd3b9b482d24a8 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 26 Feb 2026 08:49:47 +0100
Subject: [PATCH] chore: `idbg` refinements (#12691)

---
 src/Lean/Elab/Idbg.lean | 2 +-
 src/Lean/Parser/Do.lean | 2 +-
 src/Lean/Setup.lean     | 5 +++++
 3 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Elab/Idbg.lean b/src/Lean/Elab/Idbg.lean
index b601519d1d..af523ee8f9 100644
--- a/src/Lean/Elab/Idbg.lean
+++ b/src/Lean/Elab/Idbg.lean
@@ -235,7 +235,7 @@ def idbgCompileAndEval (α : Type) [Nonempty α]
   | .error msg => throw (.userError s!"idbg evalConst failed: {msg}")
 
 /-- Connect to the debug server, receive expressions, evaluate, send results. Loops forever. -/
-@[nospecialize] public def idbgClientLoop {α : Type} [Nonempty α]
+@[nospecialize, export lean_idbg_client_loop] def idbgClientLoopImpl {α : Type} [Nonempty α]
     (siteId : String) (imports : Array Import) (apply : α → String) : IO Unit := do
   let baseEnv ← idbgLoadEnv imports
   let port := idbgPort siteId
diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean
index f0c7c1fed2..4222a87cdf 100644
--- a/src/Lean/Parser/Do.lean
+++ b/src/Lean/Parser/Do.lean
@@ -63,7 +63,7 @@ def notFollowedByRedefinedTermToken :=
   -- an "open" command follows the `do`-block.
   -- If we don't add `do`, then users would have to indent `do` blocks or use `{ ... }`.
   notFollowedBy ("set_option" <|> "open" <|> "if" <|> "match" <|> "match_expr" <|> "let" <|> "let_expr" <|> "have" <|>
-      "do" <|> "dbg_trace" <|> "assert!" <|> "debug_assert!" <|> "for" <|> "unless" <|> "return" <|> symbol "try")
+      "do" <|> "dbg_trace" <|> "idbg" <|> "assert!" <|> "debug_assert!" <|> "for" <|> "unless" <|> "return" <|> symbol "try")
     "token at 'do' element"
 
 @[builtin_doElem_parser] def doLet      := leading_parser
diff --git a/src/Lean/Setup.lean b/src/Lean/Setup.lean
index fc9da73beb..b0cd4d5d32 100644
--- a/src/Lean/Setup.lean
+++ b/src/Lean/Setup.lean
@@ -33,6 +33,11 @@ structure Import where
   deriving Repr, Inhabited, ToJson, FromJson,
     BEq, Hashable -- needed by Lake (in `Lake.Load.Elab.Lean`)
 
+-- TODO: move further up into `Init` by using simpler representation for `imports`
+@[extern "lean_idbg_client_loop"]
+public opaque Idbg.idbgClientLoop {α : Type} [Nonempty α]
+  (siteId : String) (imports : Array Import) (apply : α → String) : IO Unit
+
 instance : Coe Name Import := ⟨({module := ·})⟩
 
 instance : ToString Import := ⟨fun imp =>