vscode-tlaplus
vscode-tlaplus copied to clipboard
TLA+ CommunityModules and vscode-tlaplus
The popularity of the CommunityModules warrants that we bundle (or otherwise) include its jar in the vscode extension.
Community Modules in vscode can be enabled with the following steps:
-
Download the CommunityModules.jar and CommunityModules-deps.jar from the CommunityModules release page. Be sure to save these jars to a path that vscode has access to (otherwise it fails silently).
-
Download the prerelease version of tla2tools.jar from the release page. Other releases have some issues similar to whats described here.
-
In vscode, go to the settings editor and from there go to Extensions->TLA+. In the Tlaplus › Java: Options field, add: -cp /path/to/jars/CommunityModules.jar:/path/to/jars/CommunityModules-deps.jar:/path/to/jars/tla2tools.jar

-
You can additionally specify your java path here if you have multiple versions of java installed. You must have a java version greater then 9 otherwise you will get other errors.
-
Run check model to verify that everything loads properly. You should be now able to use CommunityModules in your spec!