====== Visual Studio Code Extension ======

This is the fastest and easiest way to get started with TLA+ and TLC.

  - [[https://code.visualstudio.com/Download|Download]] and install Visual Studio Code
  - Open it, go to the Marketplace panel, find the "TLA+" extension and click "Install". Make sure to install TLA+ from TLA+ Foundation.
  - Install Java if it's not present on your computer.

That's it, you're ready to write and check your first specification!

If you're new to Visual Studio Code, its [[https://code.visualstudio.com/docs|documentation]] is a good way to start working with it.

The source code of the plugin is available on GitHub: [[https://github.com/tlaplus/vscode-tlaplus]]

------

Here you can find information on the features the extension provides and tips on how to use it efficiently.

  * If the extension is already installed, the simplest way to start working with it is described in the [[using:vscode:getting_started|Getting Started]] section.
  * Should you want to change how the extension behaves, have a look at the [[using:vscode:settings|Settings]] and [[using:vscode:setting_up_environment|Setting-up-Environment]] sections.
  * The most valuable functionality is provided by means of [[using:vscode:commands|commands]], so it’s a good idea to learn about them.
  * Something doesn’t work as you expected? Please, refer to the [[using:vscode:troubleshooting|Troubleshooting]] and [[using:vscode:caveats|Caveats]] sections, or [[https://github.com/tlaplus/vscode-tlaplus/issues/new|file an issue]] if you can’t find a solution.