| Next revision | Previous revision |
| using:vscode:installing_java [2024/10/19 19:19] – created fponzi | using:vscode:installing_java [2024/10/25 16:58] (current) – fponzi |
|---|
| ===== Why Java? ===== | ===== Why Java? ===== |
| |
| The extension uses [[https://github.com/tlaplus/tlaplus|the official TLA<html><sup></html>+<html></sup></html> tools]] to support such features as PlusCal-to-TLA<html><sup></html>+<html></sup></html> 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. | The extension uses [[https://github.com/tlaplus/tlaplus|the official TLA<sup>+</sup> tools]] to support such features as PlusCal-to-TLA<sup>+</sup> 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<html><sup></html>+<html></sup></html> tools can be used with Java 8, yet it’s strongly recommended to use Java 11 or higher. | **Attention!** At the moment, the TLA<sup>+</sup> tools can be used with Java 8, yet it’s strongly recommended to use Java 11 or higher. |
| |
| ===== Check the existing JVM installation ===== | ===== Check the existing JVM installation ===== |
| 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. | 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<html><sup></html>+<html></sup></html> 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. | To do this, open the [[https://code.visualstudio.com/docs/getstarted/settings|Settings panel]], find the TLA<sup>+</sup> 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. |
| |
fponzi