Community Modules

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!

Provide feedback