Towards a migration guide: TLA+ Toolbox → TLA+ VSCode extension

[Markus Kuppe]

Hi everyone,

for those of you who have switched from the TLA+ Toolbox to the TLA+ VS Code extension — and are enjoying it — the TLA+ project could really use your help!

We would like to create a migration guide to help others make the transition smoothly. As discussed in GitHub issue #423 [1], most of the current beginner documentation still depends heavily on the Toolbox. Since the Toolbox is now mostly in maintenance mode, that documentation is sending new TLA+ users down the legacy path.

The two environments are largely equivalent in features, but active development and improvements are now focused on the VS Code extension. In addition, VS Code offers native support for AI tools and coding assistants, which can make learning and using TLA+ more efficient and approachable.

If you have already made the move, your experience — what worked well, what caused confusion, and what you wish you had known — would be extremely valuable to others in the community.

We will use the GitHub issue to organize the work.

Thanks,
Markus

[1] https://github.com/tlaplus/vscode-tlaplus/issues/423

[Hillel Wayne]

I need to rewrite learntla to use vscode, but might be a bit before I can get to that. If this migration resource is written I can put a temporary disclaimer on relevant ltla pages.

H

--
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+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/F9663C19-3AAD-4913-AA46-C126AEB0F7EA%40lemmster.de.