Port learntla text to VSCode

[sishtiaq]

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?

[hwayne]

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

[sishtiaq]

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.

[hwayne]

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.

[hwayne]

Maybe I can make a .. vscode:: directive and use it to call out differences

[sishtiaq]

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.