Differences

This shows you the differences between two versions of the page.

--- using:vscode:migrating_from_tlatoolbox [2026/10/12 21:57] – fponzi
+++ using:vscode:migrating_from_tlatoolbox [2026/10/12 22:28] (current) – fponzi
@@ Line 2: / Line 2: @@
 TLA+ Toolbox is an IDE based on Eclipse, and for a long time it has been the official environment to work with TLA+ tools. See: https://lamport.azurewebsites.net/tla/toolbox.html
-Since around 2020 the development focus has moved to improve the VScode plugin experience. The TLA+ Toolbox has now moved to archived mode. The current bugs won't be fixed and as as dependency rots, eventually it will stop being distributed as well. Therefore it is not recommended for daily use.
+Since around 2020 the development focus has moved to improve the VScode plugin experience. The TLA+ Toolbox has now moved to archived mode and it's unmaintained. The current bugs won't be fixed and as dependency rots, eventually it will stop being distributed as well. It is therefore not recommended for daily use.
-If you haven't yet, you should consider moving to the VSCode official extension:
+If you haven't yet, you should consider moving to the [[https://marketplace.visualstudio.com/items?itemName=tlaplus.vscode-ide|VSCode official extension]] and [[https://open-vsx.org/extension/tlaplus/vscode-ide|compatible editors]]. Benefits:
   * Don't need a separated IDE to work on TLA+
@@ Line 20: / Line 20: @@
   * Quotes or short notes from users who migrated (was it easy/hard? Anything you think it's still missing?)
-  * "What I wish I knew"
   * Example workflow improvements (e.g., using GitHub Copilot to write PlusCal)