From f8af56cce4d31c5640185de9fdff1d8a99976ab9 Mon Sep 17 00:00:00 2001 From: urikirsh Date: Wed, 29 Jan 2025 21:14:05 +0200 Subject: [PATCH] branching out the evm compilers installation info --- docs/user-guide/index.md | 1 + docs/user-guide/install.md | 137 +------------------------------------ 2 files changed, 2 insertions(+), 136 deletions(-) diff --git a/docs/user-guide/index.md b/docs/user-guide/index.md index 119fc105f..11058aa8f 100644 --- a/docs/user-guide/index.md +++ b/docs/user-guide/index.md @@ -29,6 +29,7 @@ think about and write high-level properties. tutorials.md install.md +install_evm_compiler.md ci.rst running.rst properties/index.md diff --git a/docs/user-guide/install.md b/docs/user-guide/install.md index 6f62dd60a..5180277e2 100644 --- a/docs/user-guide/install.md +++ b/docs/user-guide/install.md @@ -5,7 +5,7 @@ Installation ============ -Step 1: prerequisites +Step 1: Prerequisites ---------------------
@@ -295,141 +295,6 @@ follow the next steps: source .profile ``` -(selecting-solidity-compiler)= -Step 4: Install the relevant Solidity compiler versions ---------------------------------------------------------------------------- - -The Solidity compiler (`solc`) is a verification requirement. -There are two ways to install it: via [solc-select](https://github.com/crytic/solc-select) or downloading the binary directly and adding its folder to your `PATH`. - -```{index} single: solc; solc-select -``` - -### Using `solc-select` - -
- - solc-select instructions - - * Open a terminal and install `solc-select` via `pip`: - - ```bash - pip install solc-select - ``` - - * Download the required compiler version. For example, - if you want to install version 0.8.0, run: - - ```bash - solc-select install 0.8.0 - ``` - - * Set `solc` to point to the required compiler version. For example: - - ```bash - solc-select use 0.8.0 - ``` -
- - -```{index} single: solc; solc executables -``` - -### Download binaries - -You can download the `solc` binaries directly from -[Solidity's release page on GitHub](https://github.com/ethereum/solidity/releases). - -To run the Prover, you may find it useful to add the -`solc` executables folder to your `PATH`. This way -you will not need to provide the Prover with the -full path to the `solc` executables folder every time. - -```{eval-rst} -.. dropdown:: Downloading binaries - - .. tab-set:: - - .. tab-item:: macOS - :sync: macos - - * 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 ``SolidityCertoraProver``, and open it with your favorite text editor: - - .. code-block:: bash - - sudo nano SolidityCertoraProver - - * Write the full path to the directory that contains the ``solc`` executables: - - .. code-block:: bash - - /full/path/to/solc/executable/folder - - * If needed, more than one path can be added on a single file, - just separate the path with colon a (``:``). - - * 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 - - * 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 full - path to the directory that contains the `solc` executables. - To add an additional path just separate with a colon (``:``) : - - .. code-block:: bash - - PATH="$PATH:/full/path/to/solc/executable/folder" - - * 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 -``` - -```{index} single: install; vyper -``` - -Step 5 (optional, for Vyper users): Install the Vyper compiler (`vyper`) --------------------------------------------------------------------------------- -[Vyper](https://github.com/vyperlang/vyper) is an EVM compatible Pythonic smart contract language. -Since the Certora Prover operates on the bytecode, it can be applied to any source-level language -that compiles to EVM bytecode. -We recommend to install Vyper either from PyPi (i.e., `pip install vyper`) or to get a -binary executable for the desired version. - ```{index} single: VS code; extension ```