tlaplus
TLA+ Toolbox to VSCode extension migration guide
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.
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.
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.
@FedericoPonzi Could you please create a basic structure for a page that others like @younes-io can build upon?
I've created: https://docs.tlapl.us/using:vscode:migrating_from_tlatoolbox I'll start by adding some basic information in there soon
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?
@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.