learntla-v2
learntla-v2 copied to clipboard
hwayne
Port learntla text to VSCode
TLA+ Toolbox seems clunky. All the cool kids are using VSCode! (And TLA+ is VSCode is nice and useable thanks to https://github.com/tlaplus/vscode-tlaplus.) The learntla text uses TLA+ Toolbox. But there's no direct 1-1 mapping of TLA+ Toolbox screens/fields/commands (and there are a lot of screens/fields/commands there!) to VSCode. As a specific example, it took me a bit of time to figure out where to put duplicates's (just started on your learntla website --- thanks for this) invariants and properties in the duplicate.cfg. Can the learntla text (examples, in particular) be ported to use VSCode instead?
I teach my classes in VSCode, the problem that keeps me from migrarting everything (besides laziness) is that you can't put negative numbers or sequences as constants in VScode, at least not without some file shenaniganry
ah ok. I can help with the laziness: if you file tickets here outlining what's to be done, I can pick up some of them. (And easy to do when I'm just starting your series.) VSCode issues: presumably you've filed them with the extension maintainers? They sound pretty critical to making VSCode a replacement tool.
The problem isn't with VSCode, it's with TLC. TLC's .cfg format can't accept anything besides basics numbers and sets.
To make constants with sequences or negative numbers, you need to create a separate file called, like MySpecMC.tla, and then INSTANCE MySpec WITH Constant1 <- -1, Constant2 <- <<foo, bar>>, and then define a new MySpecMC.cfg. The Toolbox does this automatically for you.
The problem...'s with TLC. TLC's .cfg format can't accept anything besides basics numbers and sets. Is there an issue on the TLC repo about this? Seems like what the Toolbox does is a workaround.
Update, I've since found that the toolbox is no longer as actively maintained so I will probably have to migrate all examples to vscode anyway