Skip to content

Expand installation instructions for PVerifier on Amazon Linux 2 #864

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
May 21, 2025
Merged

Expand installation instructions for PVerifier on Amazon Linux 2 #864

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
78 changes: 63 additions & 15 deletions Docs/docs/advanced/PVerifierLanguageExtensions/install-pverifier.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,8 @@ PVerifier requires several dependencies to be installed. Follow the steps below

```sh
sudo rpm --import https://yum.corretto.aws/corretto.key
sudo curl -L-o /etc/yum.repos.d/corretto.repo https://yum.corretto.aws/corretto.repo
sudo yum install java-11-amazon-corretto-devel
sudo curl -L -o /etc/yum.repos.d/corretto.repo https://yum.corretto.aws/corretto.repo
sudo yum install java-11-amazon-corretto-devel maven
```

??? hint "Troubleshoot: Confirm that java is correctly installed on your machine."
Expand All @@ -31,26 +31,50 @@ sudo yum install sbt

??? hint "Troubleshoot: Confirm that sbt is correctly installed on your machine."
```shell
sbt sbtVersion
sbt --version
```

If you get `sbt` command not found error, most likely, you need to add the path to `sbt` in your `PATH`.

### [Step 3] Install Z3
### [Step 3] Install .NET 8.0

Install .NET 8.0 from Microsoft:

```sh
wget https://dotnet.microsoft.com/download/dotnet/scripts/v1/dotnet-install.sh
bash ./dotnet-install.sh -c 8.0 -i $HOME/.dotnet

sudo mkdir /usr/share/dotnet/
sudo cp -r $HOME/.dotnet/* /usr/share/dotnet/
```

Then add the following line to `.zshrc` and run `source .zshrc` (or `.bashrc` if using bash):

```sh
export PATH=$HOME/.dotnet:$HOME/.dotnet/tools:$PATH
```

The purpose of copying the .NET distribution into `/usr/share/dotnet` is to make standard dotnet packages available to dotnet. If you are uncomfortable modifying a system directory, you can add the following line to your `.zshrc` or `.bashrc` instead:

```sh
export DOTNET_ROOT=$HOME/.dotnet
```

### [Step 4] Install Z3

```sh
cd ~
git clone https://github.com/Z3Prover/z3.git
cd z3
python scripts/mk_make.py --java
python scripts/mk_make.py --java
cd build; make
```

Then add the following lines to your `.zshrc` (or `.bashrc` if using bash) and run `source ~/.zshrc`:
Then add the following lines to your `.zshrc` and run `source ~/.zshrc` (or `.bashrc` if using bash):

```sh
export PATH=$PATH=$HOME/z3/build/
export LD_LIBRARY_PATH=$LD_LIBRARY_PATH=$HOME/z3/build/
export PATH=$PATH:$HOME/z3/build/
export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:$HOME/z3/build/
```

??? hint "Troubleshoot: Confirm that Z3 is correctly installed on your machine."
Expand All @@ -60,37 +84,61 @@ export LD_LIBRARY_PATH=$LD_LIBRARY_PATH=$HOME/z3/build/

If you get `z3` command not found error, most likely, you need to add the path to `z3` in your `PATH`.

### [Step 4] Install UCLID5
Note:

* Python: Building Z3 requires Python 3, but Python 2 is the default on Amazon Linux 2. If `python --version` displays version 2, try
```sh
sudo alternatives --set python `which python3`
```
or
```sh
alias python=python3
```

* G++: Building Z3 requires G++ 8 or later with support for C++20, but G++ 7 is the default on Amazon Linux 2. If `g++ --version` displays version 7, try

```sh
sudo yum install gcc10 gcc10-c++
```

to install gcc10-gcc and gcc10-g++ and replace the string `gcc` with `gcc10-` in `config.mk`.

### [Step 5] Install UCLID5

```sh
cd ~
git clone https://github.com/uclid-org/uclid.git
cd uclid
sbt update clean compile "set fork:=true" test # should fail some tests that use cvc5 and delphi
sbt update clean compile "set fork:=true" test # should fail some tests that use cvc5 and delphi
sbt universal:packageBin
unzip target/universal/uclid-0.9.5.zip
```

Then add the following line to your `.zshrc` (or `.bashrc` if using bash) and run `source ~/.zshrc`:

```sh
export PATH=$PATH=$HOME/uclid/uclid-0.9.5/bin/
export PATH=$PATH:$HOME/uclid/uclid-0.9.5/bin/
```

Note:
* Tests using cvc5 and delphi are likely to fail. If you just cut and paste the build commands into your shell, this failure may inhibit running the last two commands, so just cut and paste the last two commands into your shell again.

??? hint "Troubleshoot: Confirm that UCLID5 is correctly installed on your machine."
```shell
uclid --help
```

If you get `uclid` command not found error, most likely, you need to add the path to `uclid` in your `PATH`.

### [Step 5] Install PVerifier
### [Step 6] Install PVerifier

The following steps will build P with PVerifier by running the regular P build on the PVerifier branch of the repository.

```sh
cd ~
git clone https://github.com/p-org/P/tree/dev_p3.0/pverifier
git clone https://github.com/p-org/P
cd P
# follow regular P install instructions
git checkout dev_p3.0/pverifier
root=$(pwd)
cd $root/Bld
./build.sh
Expand All @@ -105,4 +153,4 @@ dotnet tool install P --global --add-source ./publish
p --version
```

If you get `p` command not found error, most likely, you need to add the path to `p` in your `PATH`.
If you get `p` command not found error, most likely, you need to add the path to `p` in your `PATH`.
Loading