TLA+ Toolbox to VSCode extension migration guide

[lemmy]

The TLA+ Toolbox is effectively in maintenance mode — it’s dying from bit rot. However, much of the existing documentation still refers to the Toolbox, and most beginner materials are based on it.

To address this, we should create a migration guide that helps users transition from the Toolbox to the VS Code extension, which in many respects is already more feature-rich. Thanks to @kape1395, the gap in TLAPS support has also been closed.

This migration guide is hosted at https://docs.tlapl.us/using:vscode:migrating_from_tlatoolbox, where the community can continue to update and improve it over time.

[younes-io]

how do we submit pages/contribute to https://docs.tlapl.us/ ? I've been trying to get familiar with it, it's tricky.. is there a guide? is there a repo for it?
Can we contribute using MD ? it uses some other language, I guess.

[lemmy]

@FedericoPonzi Does DocuWiki or some of its plugins support Markdown?

[FedericoPonzi]

how do we submit pages/contribute to https://docs.tlapl.us/ ? I've been trying to get familiar with it, it's tricky.. is there a guide? is there a repo for it? Can we contribute using MD ? it uses some other language, I guess.

The wiki is based on dokuwiki, there are a couple of info pages you can look up: https://docs.tlapl.us/wiki:dokuwiki and https://docs.tlapl.us/wiki:syntax

You can simply open an url you'd like to use, like: https://docs.tlapl.us/using:vscode:migration then click on the icon on the right to create a new page:

@FedericoPonzi Does DocuWiki or some of its plugins support Markdown?

As mentioned on the homepage markdown is not supported. IIRC I tried a few plugins but they were not working very well. Dokuwiki syntax is not too bad and it's easy to write stuff by using the integrated editor.

[lemmy]

@FedericoPonzi Could you please create a basic structure for a page that others like @younes-io can build upon?

[FedericoPonzi]

I've created: https://docs.tlapl.us/using:vscode:migrating_from_tlatoolbox I'll start by adding some basic information in there soon

[younes-io]

If this is the official repo of the TLA+ VC Code extension, then why aren't we using the Wiki space provided natively by Github instead of another website/domain/structure?

[lemmy]

@younes-io We discussed and weighed the decision to use a hosted DokuWiki instead of the GitHub Wiki extensively. One reason was to avoid vendor lock-in, but more importantly, we wanted a platform that doesn’t require contributors to have a GitHub account.

[inevity]

Do we need impl tla2tools.jar in the extension? I see it is located in https://github.com/tlaplus/tlaplus/tree/master/tlatools/org.lamport.tlatools

[lemmy]

Do we need impl tla2tools.jar in the extension? I see it is located in https://github.com/tlaplus/tlaplus/tree/master/tlatools/org.lamport.tlatools

Yes, the TLA+ VS Code extension does require tla2tools.jar. This JAR originates from the TLA+ repository at
https://github.com/tlaplus/tlaplus/tree/master/tlatools/org.lamport.tlatools.

For development purposes, this repository includes some older version of tla2tools.jar to satisfy the dependency locally (we don't want to inflate the size of this git repo by adding many versions of tla2tools.jar). However, this version is not what ultimately ships to users. During the build process, the GitHub Actions workflow downloads the most recent version of tla2tools.jar (along with the CommunityModules) and packages both JARs into the generated .vsix file.