From addad6f28c171c322daf6e1fa4a83a6310d8137a Mon Sep 17 00:00:00 2001 From: Marco Lampacrescia <65171491+MarcoLm993@users.noreply.github.com> Date: Fri, 14 Jun 2024 10:56:15 +0200 Subject: [PATCH] Improve deployment installation (#9) Signed-off-by: Marco Lampacrescia --- .github/workflows/build_executable.yml | 13 +++++++++ README.md | 19 ++++++++++-- docs/source/installation.rst | 40 ++++++++++++++++++++------ docs/source/tutorials.rst | 2 +- 4 files changed, 62 insertions(+), 12 deletions(-) diff --git a/.github/workflows/build_executable.yml b/.github/workflows/build_executable.yml index e16d85b..670eb7e 100644 --- a/.github/workflows/build_executable.yml +++ b/.github/workflows/build_executable.yml @@ -86,6 +86,19 @@ jobs: cd deployment cat << EOF > install.sh #!/bin/bash + # Check if --install-dependencies is set + if [[ "\$1" == "--install-dependencies" ]]; then + # Check if we need to prepend sudo + if [[ \$(id -u) -ne 0 ]]; then + SUDO=sudo DEBIAN_FRONTEND=noninteractive + else + # Required only when running in docker, as root + export DEBIAN_FRONTEND=noninteractive + fi + # Install the dependencies + \$SUDO apt update + \$SUDO apt install -y --no-install-recommends chrpath libboost-all-dev libcln-dev libgmp-dev libginac-dev libglpk-dev libhwloc-dev libz3-dev libxerces-c-dev libeigen3-dev libgtest-dev + fi SOURCE=\$( cd -- "\$( dirname -- "\${BASH_SOURCE[0]}" )" &> /dev/null && pwd ) chrpath -r \$SOURCE/3rd_party \$SOURCE/3rd_party/libspot.so.0 chrpath -r \$SOURCE/3rd_party \$SOURCE/3rd_party/libstorm.so diff --git a/README.md b/README.md index 9512405..2e95a4c 100644 --- a/README.md +++ b/README.md @@ -3,7 +3,22 @@ A Statistical Model Checker implementation building on top of STORM ## Installation -### Get the Official Storm installed +### Using deployed binaries + +We provide pre-built binaries that can be used on Ubuntu. They can be found at the [Releases page](https://github.com/convince-project/smc_storm/releases). + +To install them on your machine, extract `smc_storm_executable.tar.gz` and follow these steps: + +```bash +cd smc_storm_executable # This is the extracted archive +install.sh --install-dependencies # This flag will install all packages required by smc_storm and its dependencies +export PATH=$PATH:$PWD/bin # This way, smc_storm can be called from anywhere +smc_storm --help # Make sure the binary runs +``` + +### Compile from source + +#### Get the Official Storm installed This package needs Storm to be built on your local machine. To achieve that, follow the [official documentation](https://www.stormchecker.org/documentation/obtain-storm/build.html). We used the following command to build storm: @@ -14,7 +29,7 @@ cmake -DSTORM_USE_SPOT_SHIPPED=ON $STORM_DIR && make -j10 We recommend to use the `master` branch, since it provides the latest features as the trigonometric operators. -### Build this module +#### Build this module After cloning this repository, execute the following commands: ```bash mkdir build && cd build diff --git a/docs/source/installation.rst b/docs/source/installation.rst index 98f8c4f..5672552 100644 --- a/docs/source/installation.rst +++ b/docs/source/installation.rst @@ -4,8 +4,25 @@ Installation Guide How to install smc_storm ------------------------ +Use deployed binaries ++++++++++++++++++++++ + +We provide pre-built binaries that can be used on Ubuntu. They can be found at the `Releases page `_. + +To install them on your machine, extract `smc_storm_executable.tar.gz` and follow these steps: + +.. code-block:: bash + + cd smc_storm_executable # This is the extracted archive + install.sh --install-dependencies # This flag will install all packages required by smc_storm and its dependencies + export PATH=$PATH:$PWD/bin # This way, smc_storm can be called from anywhere + smc_storm --help # Make sure the binary runs + +Build from source ++++++++++++++++++ + Install STORM -+++++++++++++ +_____________ smc_storm needs STORM to be built on the local machine. To achieve that, follow the `official documentation `_. @@ -19,7 +36,7 @@ We used the following command to build STORM: cmake -DSTORM_USE_SPOT_SHIPPED=ON $STORM_DIR && make -j10 Install smc_storm -+++++++++++++++++ +_________________ Once STORM is installed, smc_storm can be built using the following: @@ -30,21 +47,26 @@ Once STORM is installed, smc_storm can be built using the following: cd build cmake .. -DCMAKE_BUILD_TYPE=Release && make -j4 -Make it available from anywhere -+++++++++++++++++++++++++++++++ +Make smc_storm available from anywhere +++++++++++++++++++++++++++++++++++++++ In order to be able to call smc_storm from anywhere in bash, you can add the smc_storm path to the PATH env variable: .. code-block:: bash - export PATH=$PATH:$HOME/storm_ws/smc_storm/build/bin + export PATH=$PATH: + +The path will depend on the used installation strategy: +* If you used the pre-built binaries, the path will be `/smc_storm_executable/bin` +* If you built from source, the path will be `/smc_storm/build/bin` +The `` is the directory where you extracted the pre-built binaries or where you cloned the smc_storm repository. -Verify everything is working ----------------------------- +Verify the installation works +----------------------------- -To verify that everything is working, you can run the following test from the build folder: +To verify that the binaries are able to execute, you can try to run it and check the execution terminates correctly: .. code-block:: bash - ./test_models + smc_storm --help diff --git a/docs/source/tutorials.rst b/docs/source/tutorials.rst index f67742e..6563d8d 100644 --- a/docs/source/tutorials.rst +++ b/docs/source/tutorials.rst @@ -14,7 +14,7 @@ Retrieve the available options Examples ++++++++ -Here some examples are provided, to show how to run smc_storm on the exemplary models provided in the `test/test_files` folder: +Here some examples are provided, to show how to run smc_storm on the exemplary models provided in the `test_files folder `_: .. code-block:: bash