vscode-tlaplus
vscode-tlaplus copied to clipboard
tlaplus
TLA+ language support for Visual Studio Code
I found it quite unclear how to run TLC on multicore. Here is the solution I figured out and I put it here for others that might need: Set -...
In the toolbox if the generated TLA code has an error its often possible to jump to the line of pluscal that is the source for the generated error. Is...
The `TlaDocumentSymbolsProvider` stumbles on operators while parsing constants and doesn't report them as model symbols. As a result, const operator names don't appear in the outline panel and in completion...
The extension now supports on-type formatting, i.e. automatic code indentation while the user is typing. It would be great to also support formatting of the selected code blocks (including the...
Hi - When I followed the Getting Started, I couldn't find either "Create new module (TLA+)" or "Create PlusCal block (TLA+)" snippet from the drop-down list. So I wonder how...
Hi - I get the following message at the end of model checking execution. "End of statistics (please note that for performance reasons large models are best checked with coverage...
I'm trying to run model checking on TLA+ spec at https://github.com/joshuazh-x/raft/blob/trace-validation/tla/MCetcdraft.tla using simulation mode. The output shows progresses but the status panel in vscode stuck in computing initial states. I...
@alygin ``` [check if VSCODE_MARKETPLACE_TOKEN is set in github secrets](https://github.com/tlaplus/vscode-tlaplus/actions/runs/3252287934/jobs/5338328786#step:2:9) The `set-output` command is deprecated and will be disabled soon. Please upgrade to using Environment Files. For more information see:...
The released version of this extension, found at [alygin.vscode-tlaplus](https://marketplace.visualstudio.com/items?itemName=alygin.vscode-tlaplus), is severely outdated (last update was in 2021). I suggest to replace the released version with the "nightly build" version, available...
This is related to https://github.com/tlaplus/tlapm/pull/93. The extension could suggest a user download and install the proper version of the TLAPS/LSP. We should return to this when the LSP support in...
