Skip to content

feat: idbg interactive debug expression evaluator#12648

Merged
Kha merged 8 commits intoleanprover:masterfrom
Kha:idbg
Feb 23, 2026
Merged

feat: idbg interactive debug expression evaluator#12648
Kha merged 8 commits intoleanprover:masterfrom
Kha:idbg

Conversation

@Kha
Copy link
Copy Markdown
Member

@Kha Kha commented Feb 23, 2026

This PR adds the experimental idbg e, a new do-element (and term) syntax for live debugging between the language server and a running compiled Lean program.

When placed in a do block, idbg captures all local variables in scope and expression e, then:

  • In the language server: starts a TCP server on localhost waiting for the running program to
    connect; the editor will mark this part of the program as "in progress" during this wait but that
    will not block lake build of the project.
  • In the compiled program: on first execution of the idbg call site, connects to the server,
    receives the expression, compiles and evaluates it using the program's actual runtime values, and
    sends the repr result back.

The result is displayed as an info diagnostic on the idbg keyword. The expression e can be
edited while the program is running - each edit triggers re-elaboration of e, a new TCP exchange,
and an updated result. This makes idbg a live REPL for inspecting and experimenting with
program state at a specific point in execution. Only when idbg is inserted, moved, or removed does
the program need to be recompiled and restarted.

Known Limitations

  • The program will poll for the server for up to 10 minutes and needs to be killed manually
    otherwise.
  • Use of multiple idbg at once untested, likely too much overhead from overlapping imports without
    further changes.
  • LEAN_PATH must be properly set up so compiled program can import its origin module.
  • Untested on Windows and macOS.

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Feb 23, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Feb 23, 2026

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5115229be20c18d5e9eb923dd10470b9633e8299 --onto 2e7fe7e79d151ee91039f086b8036252cdf9b725. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-23 11:56:39)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5115229be20c18d5e9eb923dd10470b9633e8299 --onto e7e3588c973226e85d79ed0f3154cfca79b61c6f. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-23 15:52:11)

@leanprover-bot
Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 5115229be20c18d5e9eb923dd10470b9633e8299 --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-02-23 11:56:41)

@Kha Kha added this pull request to the merge queue Feb 23, 2026
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Feb 23, 2026
@Kha Kha enabled auto-merge February 23, 2026 17:14
@Kha Kha added this pull request to the merge queue Feb 23, 2026
Merged via the queue into leanprover:master with commit 8f80881 Feb 23, 2026
15 checks passed
@Kha Kha deleted the idbg branch February 23, 2026 17:51
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-other toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants