```{index} single: install
```
(installation)=
Installation
============
Step 1: Prerequisites
---------------------
Python3.8.16 or newer
Check your Python3 version by executing the following command on the
terminal:
```bash
python3 --version
```
If the version is < 3.8.16, follow the [Python installation guide][pythonInstall] to upgrade.
[pythonInstall]: https://wiki.python.org/moin/BeginnersGuide/Download
Java Development Kit (JDK) 11 or newer
Check your Java version by executing the following command on the terminal:
```bash
java -version
```
If the version is < 11, download and install Java version 11 or later from
[Oracle](https://www.oracle.com/java/technologies/downloads/).
```{index} single: solc
```
Solidity compiler (ideally v0.5 and up)
* We recommend using [solc-select](https://github.com/crytic/solc-select)
to download and switch between Solidity compiler versions.
* You can also download the Solidity compiler binaries from the
[official Solidity repository](https://github.com/ethereum/solidity/releases) on GitHub.
It is best to place all the `solc` binaries in the same path.
* Certora employees can clone the `CVT_Executables` repository suitable for
their OS from [GitHub](https://github.com/orgs/Certora/repositories).
Step 2: Install the Certora Prover package
------------------------------------------
```{tip}
It is always recommended to use a Python virtual environment,
such as [venv][venv] or [virtualenv][virtualenv],
when installing a Python package.
```
[venv]: https://docs.python.org/3.10/library/venv.html
Execute the following command at the terminal to install the Prover:
```bash
pip3 install certora-cli
```
```{caution}
Note that the terminal may prompt you with a warning that some files, e.g.
python3.x, are not included in the `PATH`, and should be added. Add these files
to `PATH` to avoid errors.
```
The following section presents some, but maybe not all, possible warnings that
can arise during installation and how to deal with them:
```{eval-rst}
.. dropdown:: Troubleshooting warnings
.. tab-set::
.. tab-item:: macOS
:sync: macos
.. code-block:: text
:caption: The warning
The script certoraRun is installed in /Users//Library/Python/3.8/bin
which is not on PATH. Consider adding this directory to PATH.
* Open a terminal and move to the :file:`etc/paths.d` directory from root:
.. code-block:: bash
cd /etc/paths.d
* Use root privileges to create a file with an informative name such as
``PythonForProver``, and open it with your favorite text editor:
.. code-block:: bash
sudo nano PythonForProver
* Write the specified path from the warning:
.. code-block:: bash
/specified/path/in/warning
* If needed, more than one path can be added on a single file,
just separate the path with a colon (``:``).
* Quit the terminal to load the new addition to ``$PATH``,
and reopen to check that the ``$PATH`` was updated correctly:
.. code-block:: bash
echo $PATH
.. tab-item:: Linux
:sync: linux
.. code-block:: text
:caption: The warning
The script certoraRun is installed in /home//.local/bin
which is not on PATH. Consider adding this directory to PATH.
* Open a terminal and make sure you're in the home directory:
.. code-block:: bash
cd ~
* open the .profile file with your favorite text editor:
.. code-block:: bash
nano .profile
* At the bottom of the file, add to ``PATH="..."`` the specified path
from the warning. To add an additional path just separate with a colon (`:`) :
.. code-block:: bash
PATH="$PATH:/specified/path/in/warning"
* You can make sure that the file was modified correctly by opening it again
with the text editor:
.. code-block:: bash
nano .profile
* Make sure to apply the changes to the ``$PATH`` by executing the script:
.. code-block:: bash
source .profile
```
```{eval-rst}
.. index::
single: install; beta version
single: beta version
```
(beta-install)=
## Installing the beta version (optional)
If you wish to install a pre-release version, you can do so by installing
`certora-cli-beta` instead of `certora-cli`. We do not recommend having both
packages installed simultaneously, so you should remove the `certora-cli`
package before installing `certora-cli-beta`:
```sh
pip uninstall certora-cli
pip install certora-cli-beta
```
If you wish to easily switch between the beta and the production versions, you
can use a [python virtual environment][virtualenv]:
[virtualenv]: https://virtualenv.pypa.io/en/latest/
```sh
pip install virtualenv
virtualenv certora-beta
source certora-beta/bin/activate
pip3 install certora-cli-beta
```
You can then switch to the standard CVL release by running `deactivate`, and
back to the beta release using `certora-beta/bin/activate`.
(installation-step-3)=
Step 3: Set the personal access key as an environment variable
-------------------------------------------------------------
The Certora Prover requires a personal access key.
You can get a free personal access key by registering on the
[Certora website](https://www.certora.com/signup?plan=prover).
Before running the Prover,
you should register your access key as a system variable.
To do so on macOS or Linux machines,
execute the following command on the terminal:
```bash
export CERTORAKEY=
```
This command sets a temporary variable that will be unset once the terminal is
closed. We recommended storing the access key in an environment variable named
`CERTORAKEY`. This way, you will no longer need to execute the above command
whenever you open a terminal. To set an environment variable permanently,
follow the next steps:
```{eval-rst}
.. tab-set::
.. tab-item:: macOS
:sync: macos
* Open a terminal and make sure you're in the home directory:
.. code-block:: bash
cd ~
* Create a file with the name ``.zshenv`` and open it with your favorite text editor:
.. code-block:: bash
nano .zshenv
* Write the export command from the beginning of step 3,
save and quit (``ctrl+x`` on ``nano``).
* You can make sure that the file was created correctly by
seeing it listed on the directory or by opening it again with the text editor:
.. code-block:: bash
ls -a
OR
.. code-block:: bash
nano .zshenv
* Make sure to apply the environment variable you've just created by executing the script:
.. code-block:: bash
source .zshenv
When running the Certora Prover in the Visual Studio Code Extension, you may need
to restart VSCode or your computer.
.. tab-item:: Linux
:sync: linux
* Open a terminal and make sure you're in the home directory:
.. code-block:: bash
cd ~
* open the .profile file with your favorite text editor:
.. code-block:: bash
nano .profile
* At the bottom of the file, under the ``PATH="..."`` insert
the export command from the beginning of step 3, save and quit (``ctrl+x`` on ``nano``).
* You can make sure that the file was modified correctly by
opening it again with the text editor:
.. code-block:: bash
nano .profile
* Make sure to apply the environment variable you've just created by executing the script:
.. code-block:: bash
source .profile
```
Step 4 (for GitHub users): Configure Syntax Highlighting
--------------------------------------------------------
[Follow our guide](github_highlighting.md) to configure syntax highlighting on GitHub for CVL and configuration files.