====== Installing Java ======
===== Why Java? =====
The extension uses [[https://github.com/tlaplus/tlaplus|the official TLA+ tools]] to support such features as PlusCal-to-TLA+ translation, module parsing, model checking etc. These tools need JVM (Java Virtual Machine) to run, and the extension doesn’t come with a JVM onboard. Thus, it requires a JVM to be installed on the user’s computer.
**Attention!** At the moment, the TLA+ tools can be used with Java 8, yet it’s strongly recommended to use Java 11 or higher.
===== Check the existing JVM installation =====
The simplest way to check if you already have a JVM installed is to run the following command in the command line:
java --version
If there’s a JVM on your computer, and it’s properly configured, you’ll see the information about its version. Version ''%%1.8%%'' is what we call Java 8 here.
BTW, the extension performs this check for you from time to time and warns you if something goes wrong.
===== Install JVM =====
If there’s no JVM on your computer, you can download and install one of the distributions. The most popular among them are:
* [[https://adoptopenjdk.net/|AdoptOpenJDK]] — the TLA+ Toolbox uses this one.
* [[https://www.graalvm.org/downloads/|GraalVM]] — a JVM with a brand-new compiler, works faster in most cases.
* [[https://docs.aws.amazon.com/corretto/latest/corretto-11-ug/downloads-list.html|Amazon Corretto]] — the JVM distribution from Amazon.
===== Configure the Extension =====
Sometimes, you may not want to use the extension with your globally enabled JVM (the one that is executed when you execute the ''%%java%%'' command in the command line). In such cases you need to tell the extension where to find the JVM you want to use.
To do this, open the [[https://code.visualstudio.com/docs/getstarted/settings|Settings panel]], find the TLA+ group of setting, and provide the home directory of your JVM in the ''%%Java: Home%%'' setting. Be careful, the JVM home directory is the directory where the whole JVM resides, not the full path to the ''%%java%%'' executable.