using:vscode:migrating_from_tlatoolbox

This is an old revision of the document!


Migrating from TLA+ Toolbox

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.

If you haven't yet, you should consider moving to the VSCode official extension: * Don't need a separated IDE to work on TLA+ * Extension updates in almost real time without extra steps * Matched feature set: we even have TLAPS integrated. * Developers ready to take your feature requests and feedback.

  • using/vscode/migrating_from_tlatoolbox.1760128208.txt.gz
  • Last modified: 2025/10/10 20:30
  • by fponzi