[tlaplus] New VSCode debugger setup, unsure what's missing

[Brian Curtin <brian.curtin@xxxxxxxxx>]

Hey all,

It's been a while since I've setup a new dev env, and the VSCode work that's been done in the last while looks fantastic. I'm really interested in the interactive state space and breakpoints from the screencasts like [0] .

The env is very up to date, as follows:

* Java version: java 25.0.4 2026-07-21 LTS

* VSCode version: 1.133.0 [2026-08-11T22:14:08Z (16 hrs ago)]

* tlaplus.vscode-ide version: 2026.8.22255 (2 days ago)

Something I can't really figure out is the Run and Debug pane of VSCode to initiate a debugger to hit breakpoints and step in/out/over, either invoked by the green button, or hitting F5 when on a module. In the screencast there is some debugger config setup, in that case for an EWD998App which I've seen Markus talk about. 

I can right click on a .tla file and choose "Check model with TLC" which works, but doesn't invoke it in the debugger. The "Add configuration..." debugger dropdown doesn't seem to know about TLA+/TLC; it just has Python, Node, and some default web stuff. I can choose to install an extension from there, but this is already installed. I've also looked at a launch.json, which I recall doing in the past for other things, but that seems to require host/port settings for attaching to a remote debugger, best I can tell.

Does anyone have any configuration details that can bridge the gap to where I am? Happy to update the docs along the way.

Thanks,

Brian Curtin

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/83cfa57d-5d8a-45c5-8957-c948086aa8efn%40googlegroups.com.