From 513550b75ceb23c9a9c4be2921d19f88b82bd80e Mon Sep 17 00:00:00 2001 From: Maris Galesloot Date: Fri, 24 Nov 2023 13:16:28 +0100 Subject: [PATCH 1/4] New dockerfiles and build definition --- .dockerignore | 33 ++++++ .github/workflows/buildtest.yml | 71 ++++++++++++ Dockerfile | 102 ++++++++++-------- ...ile => synthesis-specific-storm.dockerfile | 93 +++++++--------- 4 files changed, 202 insertions(+), 97 deletions(-) create mode 100644 .dockerignore create mode 100644 .github/workflows/buildtest.yml rename synthesis.dockerfile => synthesis-specific-storm.dockerfile (51%) diff --git a/.dockerignore b/.dockerignore new file mode 100644 index 000000000..7ef6eafb4 --- /dev/null +++ b/.dockerignore @@ -0,0 +1,33 @@ +*.dockerfile +*Dockerfile +.devcontainer +.vscode +.venv +__pycache__/ + +env/ +prerequisites/ +storm/ +stormpy/ +experiments/ + +#Git files +.git +.github +.gitignore +#The remainder is based on .gitignore +**/*.so +**/*.py[cod] +lib/**/_config.py +**/.eggs/ +**/*.egg-info/ +**/build/ +**/dist/ +**/.idea/ +**/__pycache__/ +**/_build/ +**/.pytest_cache/ +**/.idea/ +**/cmake-build-debug/ + +**/.DS_Store diff --git a/.github/workflows/buildtest.yml b/.github/workflows/buildtest.yml new file mode 100644 index 000000000..8f73d325c --- /dev/null +++ b/.github/workflows/buildtest.yml @@ -0,0 +1,71 @@ +name: Build Test +# Builds and tests stormpy with different versions of Storm +# also deploys images to Dockerhub + +on: + push: + branches: + - master + schedule: + # run weekly + - cron: '0 10 * * 3' + # needed to trigger the workflow manually + workflow_dispatch: + pull_request: + +env: + GIT_URL: "${{ github.server_url }}/${{ github.repository }}.git" + BRANCH: "${{ github.ref }}" + # GitHub runners currently have two cores + NR_JOBS: "2" + +jobs: + deploytemp: + name: Test and Deploy on latest using specific Storm commit (${{ matrix.buildType.name }}) + runs-on: ubuntu-latest + strategy: + matrix: + buildType: + - {name: "Release", imageName : "randriu/paynt", dockerTag: "temp", buildArgs: "BUILD_TYPE=Release", setupArgs: "", stormCommit : "dc7960b8f0222793b591f3d6489e2f6c7da1278f"} + fail-fast: false + steps: + - name: Git clone + uses: actions/checkout@v4 + - name: Build paynt from Dockerfile + run: docker build -t ${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }} . -f fixed-storm-commit.dockerfile --build-arg storm_sha=${{ matrix.buildType.stormCommit }} --build-arg build_type=${{ matrix.buildType.buildArgs }} --build-arg setup_args=${{ matrix.buildType.setupArgs }} --build-arg setup_args_pycarl=${{ matrix.buildType.setupArgs }} --build-arg no_threads=${NR_JOBS} + - name: Build image for learner + run: docker build -t ${{ matrix.buildType.imageName }}-learner:${{ matrix.buildType.dockerTag }} . -f paynt-learner.dockerfile + - name: Login into docker + # Only login if using master on original repo (and not for pull requests or forks) + if: github.repository_owner == 'randriu' && github.ref == 'refs/heads/master' + run: echo '${{ secrets.STORMPY_CI_DOCKER_PASSWORD }}' | docker login -u randriu --password-stdin + - name: Deploy paynt with specific Storm version + # Only deploy if using master on original repo (and not for pull requests or forks) + if: github.repository_owner == 'randriu' && github.ref == 'refs/heads/master' + run: docker push ${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }} + - name: Deploy paynt with specific Storm version and learner dependencies + # Only deploy if using master on original repo (and not for pull requests or forks) + if: github.repository_owner == 'randriu' && github.ref == 'refs/heads/master' + run: docker push ${{ matrix.buildType.imageName }}-learner:${{ matrix.buildType.dockerTag }} + + deploy: + name: Deploy on latest (${{ matrix.buildType.name }}) + runs-on: ubuntu-latest + strategy: + matrix: + buildType: + - {name: "Release", imageName : "randriu/paynt", dockerTag: "latest", stormTag: "ci", buildArgs: "BUILD_TYPE=Release", setupArgs: ""} + fail-fast: false + steps: + - name: Git clone + uses: actions/checkout@v4 + - name: Build stormpy from Dockerfile + run: docker build -t ${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }} . --build-arg STORM_BASE=movesrwth/storm:${{ matrix.buildType.stormTag }} --build-arg build_type=${{ matrix.buildType.buildArgs }} --build-arg setup_args=${{ matrix.buildType.setupArgs }} --build-arg setup_args_pycarl=${{ matrix.buildType.setupArgs }} --build-arg no_threads=${NR_JOBS} + - name: Login into docker + # Only login if using master on original repo (and not for pull requests or forks) + if: github.repository_owner == 'randriu' && github.ref == 'refs/heads/synthesis' + run: echo '${{ secrets.STORMPY_CI_DOCKER_PASSWORD }}' | docker login -u randriu --password-stdin + - name: Deploy stormpy + # Only deploy if using master on original repo (and not for pull requests or forks) + if: github.repository_owner == 'randriu' && github.ref == 'refs/heads/synthesis' + run: docker push ${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }} \ No newline at end of file diff --git a/Dockerfile b/Dockerfile index 0dcfbd24d..3c6e38a52 100644 --- a/Dockerfile +++ b/Dockerfile @@ -1,58 +1,72 @@ -# the docker image can be built by executing: -# docker build -t . -# to enable multi-thread compilation, use --build-arg threads= +FROM movesrwth/storm:ci -FROM ubuntu -MAINTAINER Roman Andriushchenko -ARG threads=1 +# Install dependencies +###################### +# Uncomment to update packages beforehand +RUN apt-get update -qq +RUN apt-get install -y --no-install-recommends \ + uuid-dev \ + python3 \ + python3-venv +# CMake build type +ARG build_type=Release +# Additional arguments for compiling stormpy +ARG setup_args="" +# Additional arguments for compiling pycarl +ARG setup_args_pycarl="" +# Number of threads to use for parallel compilation +ARG no_threads=2 -# execute bash when running the container -ENTRYPOINT ["/bin/bash"] +# WORKDIR /opt/ -# to prevent texlive from asking our geographical area -ENV DEBIAN_FRONTEND noninteractive +# Obtain carl-parser from public repository +# RUN git clone https://github.com/moves-rwth/carl-parser.git -# install dependencies -RUN apt update -RUN apt install -y build-essential git automake cmake libboost-all-dev libcln-dev libgmp-dev libginac-dev libglpk-dev libhwloc-dev libz3-dev libxerces-c-dev libeigen3-dev maven uuid-dev python3-dev libffi-dev libssl-dev python3-pip python3-venv vim texlive-pictures -RUN pip3 install pytest pytest-runner pytest-cov numpy scipy pysmt z3-solver click toml Cython scikit-build +# # Switch to build directory +# RUN mkdir -p /opt/carl-parser/build +# WORKDIR /opt/carl-parser/build +# # Configure carl-parser +# RUN cmake .. -DCMAKE_BUILD_TYPE=$build_type -# main directory -WORKDIR /synthesis +# # Build carl-parser +# RUN make carl-parser -j $no_threads -# download everything -# using --depth 1 to make the download faster and the image smaller -WORKDIR /synthesis/prerequisites -RUN git clone --depth 1 https://github.com/moves-rwth/pycarl.git pycarl -RUN git clone --depth 1 --branch cvc5-1.0.0 https://github.com/cvc5/cvc5.git cvc5 -WORKDIR /synthesis -RUN git clone --depth 1 https://github.com/moves-rwth/storm.git storm -RUN git clone --depth 1 --branch synthesis https://github.com/randriu/stormpy.git stormpy -RUN git clone --depth 1 https://github.com/randriu/synthesis.git paynt +# Set-up virtual environment +############################ +ENV VIRTUAL_ENV=/opt/venv +RUN python3 -m venv $VIRTUAL_ENV +ENV PATH="$VIRTUAL_ENV/bin:$PATH" +RUN pip install -U pip setuptools wheel +# Build pycarl +############## +WORKDIR /opt/pycarl -# build storm -WORKDIR /synthesis/storm/build -RUN cmake .. -RUN make storm-main storm-pomdp --jobs $threads -ENV PATH="/synthesis/storm/build/bin:$PATH" +# Obtain latest version of pycarl from public repository +RUN git clone --depth 1 https://github.com/moves-rwth/pycarl.git . -# build pycarl -WORKDIR /synthesis/prerequisites/pycarl -RUN python3 setup.py build_ext --jobs $threads develop +# Build pycarl +RUN python setup.py build_ext $setup_args_pycarl -j $no_threads develop -# building cvc5 is slow and hybrid is rarely used, so you may skip it and use z3 instead -#WORKDIR /synthesis/prerequisites/cvc5 -#RUN ./configure.sh --prefix="." --auto-download --python-bindings -#WORKDIR /synthesis/prerequisites/cvc5/build -#RUN make --jobs $threads -#RUN make install +# Build stormpy +############### +WORKDIR /opt/stormpy -# build stormpy -WORKDIR /synthesis/stormpy -RUN python3 setup.py build_ext --storm-dir /synthesis/storm/build --jobs $threads develop +# Copy the content of the current local stormpy repository into the Docker image +RUN git clone --depth 1 --branch synthesis https://github.com/randriu/stormpy.git . -# set the initial folder -WORKDIR /synthesis/paynt +# Build stormpy +RUN python setup.py build_ext $setup_args -j $no_threads develop + +# Paynt dependencies +RUN pip install pysmt z3-solver click numpy + +# Build paynt +############# +WORKDIR /opt/paynt + +COPY . . + +RUN pip install -e . diff --git a/synthesis.dockerfile b/synthesis-specific-storm.dockerfile similarity index 51% rename from synthesis.dockerfile rename to synthesis-specific-storm.dockerfile index b80fbea94..54d7ca644 100644 --- a/synthesis.dockerfile +++ b/synthesis-specific-storm.dockerfile @@ -1,98 +1,85 @@ -# Base Dockerfile for using stormpy -################################### -# The Docker image can be built by executing: -# docker build -t yourusername/stormpy . -# A different Storm base image can be set from the commandline with: -# --build-arg STORM_BASE= - -# Set Storm base image -ARG STORM_BASE=movesrwth/storm:stable -FROM $STORM_BASE - - -# Configuration arguments -######################### -# The arguments can be set from the commandline with: -# --build-arg = - -# CMake build type -ARG build_type=Release -# Additional arguments for compiling stormpy -ARG setup_args="" -# Additional arguments for compiling pycarl -ARG setup_args_pycarl="" -# Number of threads to use for parallel compilation -ARG no_threads=2 - +FROM movesrwth/storm-basesystem:latest # Install dependencies ###################### # Uncomment to update packages beforehand RUN apt-get update -qq RUN apt-get install -y --no-install-recommends \ - maven \ uuid-dev \ python3 \ python3-venv -# Packages maven and uuid-dev are required for carl-parser +# CMake build type +ARG build_type=Release +# Additional arguments for compiling stormpy +ARG setup_args="" +# Additional arguments for compiling pycarl +ARG setup_args_pycarl="" +# Number of threads to use for parallel compilation +ARG no_threads=2 +# Specific storm git commit revision SHA +ARG storm_sha=dc7960b8f0222793b591f3d6489e2f6c7da1278f -# Build carl-parser -################### WORKDIR /opt/ +RUN git clone https://github.com/moves-rwth/storm.git storm +WORKDIR /opt/storm/build +RUN git reset --hard $storm_sha +RUN cmake .. -DCMAKE_BUILD_TYPE=$build_type +RUN make storm-main storm-pomdp --jobs $no_threads +ENV PATH="/opt/storm/build/bin:$PATH" # Obtain carl-parser from public repository -RUN git clone --depth 1 https://github.com/moves-rwth/carl-parser.git +# RUN git clone https://github.com/moves-rwth/carl-parser.git -# Switch to build directory -RUN mkdir -p /opt/carl-parser/build -WORKDIR /opt/carl-parser/build +# # Switch to build directory +# RUN mkdir -p /opt/carl-parser/build +# WORKDIR /opt/carl-parser/build -# Configure carl-parser -RUN cmake .. -DCMAKE_BUILD_TYPE=$build_type +# # Configure carl-parser +# RUN cmake .. -DCMAKE_BUILD_TYPE=$build_type -# Build carl-parser -RUN make carl-parser -j $no_threads +# # Build carl-parser +# RUN make carl-parser -j $no_threads # Set-up virtual environment ############################ ENV VIRTUAL_ENV=/opt/venv -RUN python3 -m venv --upgrade-deps $VIRTUAL_ENV +RUN python3 -m venv $VIRTUAL_ENV ENV PATH="$VIRTUAL_ENV/bin:$PATH" - +RUN pip install -U pip setuptools wheel # Build pycarl ############## -WORKDIR /opt/ +WORKDIR /opt/pycarl # Obtain latest version of pycarl from public repository -RUN git clone --depth 1 https://github.com/moves-rwth/pycarl.git - -# Switch to pycarl directory -WORKDIR /opt/pycarl +RUN git clone --depth 1 https://github.com/moves-rwth/pycarl.git . # Build pycarl RUN python setup.py build_ext $setup_args_pycarl -j $no_threads develop - # Build stormpy ############### -RUN mkdir /opt/stormpy WORKDIR /opt/stormpy -# Copy the content of the synthesis repository into the Docker image +# Copy the content of the current local stormpy repository into the Docker image RUN git clone --depth 1 --branch synthesis https://github.com/randriu/stormpy.git . # Build stormpy RUN python setup.py build_ext $setup_args -j $no_threads develop +# Additional dependencies +########################## + +RUN pip install -U pip setuptools wheel numpy + +# Paynt / extra dependencies +RUN pip install pysmt z3-solver click + # Build paynt ############# WORKDIR /opt/paynt -COPY . /opt/paynt - -# Paynt / extra dependencies -RUN pip install pytest pytest-runner pytest-cov numpy scipy pysmt z3-solver click toml Cython scikit-build +COPY . . -RUN pip install . +RUN pip install -e . From 32063c0d2d82f6dd71830c13d46608d7f79b6e89 Mon Sep 17 00:00:00 2001 From: Maris Galesloot Date: Fri, 24 Nov 2023 13:18:38 +0100 Subject: [PATCH 2/4] Add Dockerfiles --- .github/workflows/buildtest.yml | 2 +- paynt-learner.dockerfile | 6 ++++++ ...ific-storm.dockerfile => paynt-specific-storm.dockerfile | 0 3 files changed, 7 insertions(+), 1 deletion(-) create mode 100644 paynt-learner.dockerfile rename synthesis-specific-storm.dockerfile => paynt-specific-storm.dockerfile (100%) diff --git a/.github/workflows/buildtest.yml b/.github/workflows/buildtest.yml index 8f73d325c..d96bdee69 100644 --- a/.github/workflows/buildtest.yml +++ b/.github/workflows/buildtest.yml @@ -32,7 +32,7 @@ jobs: - name: Git clone uses: actions/checkout@v4 - name: Build paynt from Dockerfile - run: docker build -t ${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }} . -f fixed-storm-commit.dockerfile --build-arg storm_sha=${{ matrix.buildType.stormCommit }} --build-arg build_type=${{ matrix.buildType.buildArgs }} --build-arg setup_args=${{ matrix.buildType.setupArgs }} --build-arg setup_args_pycarl=${{ matrix.buildType.setupArgs }} --build-arg no_threads=${NR_JOBS} + run: docker build -t ${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }} . -f paynt-specific-storm.dockerfile --build-arg storm_sha=${{ matrix.buildType.stormCommit }} --build-arg build_type=${{ matrix.buildType.buildArgs }} --build-arg setup_args=${{ matrix.buildType.setupArgs }} --build-arg setup_args_pycarl=${{ matrix.buildType.setupArgs }} --build-arg no_threads=${NR_JOBS} - name: Build image for learner run: docker build -t ${{ matrix.buildType.imageName }}-learner:${{ matrix.buildType.dockerTag }} . -f paynt-learner.dockerfile - name: Login into docker diff --git a/paynt-learner.dockerfile b/paynt-learner.dockerfile new file mode 100644 index 000000000..ffa73da81 --- /dev/null +++ b/paynt-learner.dockerfile @@ -0,0 +1,6 @@ +ARG paynt-base=randriu/paynt:ci +FROM paynt-base + +RUN pip install torch --index-url https://download.pytorch.org/whl/cpu + +RUN pip install ipykernel joblib tensorboard diff --git a/synthesis-specific-storm.dockerfile b/paynt-specific-storm.dockerfile similarity index 100% rename from synthesis-specific-storm.dockerfile rename to paynt-specific-storm.dockerfile From eb83729d139f8c3cc2a15c322a025e2174408662 Mon Sep 17 00:00:00 2001 From: Maris Galesloot Date: Fri, 24 Nov 2023 13:22:15 +0100 Subject: [PATCH 3/4] Build also latest image for learner --- .github/workflows/buildtest.yml | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/.github/workflows/buildtest.yml b/.github/workflows/buildtest.yml index d96bdee69..5515b4d43 100644 --- a/.github/workflows/buildtest.yml +++ b/.github/workflows/buildtest.yml @@ -34,7 +34,7 @@ jobs: - name: Build paynt from Dockerfile run: docker build -t ${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }} . -f paynt-specific-storm.dockerfile --build-arg storm_sha=${{ matrix.buildType.stormCommit }} --build-arg build_type=${{ matrix.buildType.buildArgs }} --build-arg setup_args=${{ matrix.buildType.setupArgs }} --build-arg setup_args_pycarl=${{ matrix.buildType.setupArgs }} --build-arg no_threads=${NR_JOBS} - name: Build image for learner - run: docker build -t ${{ matrix.buildType.imageName }}-learner:${{ matrix.buildType.dockerTag }} . -f paynt-learner.dockerfile + run: docker build -t ${{ matrix.buildType.imageName }}-learner:${{ matrix.buildType.dockerTag }} . -f paynt-learner.dockerfile --build-arg paynt-base=${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }} - name: Login into docker # Only login if using master on original repo (and not for pull requests or forks) if: github.repository_owner == 'randriu' && github.ref == 'refs/heads/master' @@ -61,11 +61,17 @@ jobs: uses: actions/checkout@v4 - name: Build stormpy from Dockerfile run: docker build -t ${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }} . --build-arg STORM_BASE=movesrwth/storm:${{ matrix.buildType.stormTag }} --build-arg build_type=${{ matrix.buildType.buildArgs }} --build-arg setup_args=${{ matrix.buildType.setupArgs }} --build-arg setup_args_pycarl=${{ matrix.buildType.setupArgs }} --build-arg no_threads=${NR_JOBS} + - name: Build image for learner + run: docker build -t ${{ matrix.buildType.imageName }}-learner:${{ matrix.buildType.dockerTag }} . -f paynt-learner.dockerfile --build-arg paynt-base=${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }} - name: Login into docker # Only login if using master on original repo (and not for pull requests or forks) - if: github.repository_owner == 'randriu' && github.ref == 'refs/heads/synthesis' + if: github.repository_owner == 'randriu' && github.ref == 'refs/heads/master' run: echo '${{ secrets.STORMPY_CI_DOCKER_PASSWORD }}' | docker login -u randriu --password-stdin - - name: Deploy stormpy + - name: Deploy paynt + # Only deploy if using master on original repo (and not for pull requests or forks) + if: github.repository_owner == 'randriu' && github.ref == 'refs/heads/master' + run: docker push ${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }} + - name: Deploy paynt with learner dependencies # Only deploy if using master on original repo (and not for pull requests or forks) - if: github.repository_owner == 'randriu' && github.ref == 'refs/heads/synthesis' - run: docker push ${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }} \ No newline at end of file + if: github.repository_owner == 'randriu' && github.ref == 'refs/heads/master' + run: docker push ${{ matrix.buildType.imageName }}-learner:${{ matrix.buildType.dockerTag }} \ No newline at end of file From dda25dddb8949d80e1e973ea546a9208dd20b123 Mon Sep 17 00:00:00 2001 From: Maris Galesloot Date: Fri, 24 Nov 2023 15:55:12 +0100 Subject: [PATCH 4/4] Fix typo's --- .github/workflows/buildtest.yml | 4 ++-- paynt-learner.dockerfile | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/buildtest.yml b/.github/workflows/buildtest.yml index 5515b4d43..e428c5ad1 100644 --- a/.github/workflows/buildtest.yml +++ b/.github/workflows/buildtest.yml @@ -34,7 +34,7 @@ jobs: - name: Build paynt from Dockerfile run: docker build -t ${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }} . -f paynt-specific-storm.dockerfile --build-arg storm_sha=${{ matrix.buildType.stormCommit }} --build-arg build_type=${{ matrix.buildType.buildArgs }} --build-arg setup_args=${{ matrix.buildType.setupArgs }} --build-arg setup_args_pycarl=${{ matrix.buildType.setupArgs }} --build-arg no_threads=${NR_JOBS} - name: Build image for learner - run: docker build -t ${{ matrix.buildType.imageName }}-learner:${{ matrix.buildType.dockerTag }} . -f paynt-learner.dockerfile --build-arg paynt-base=${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }} + run: docker build -t ${{ matrix.buildType.imageName }}-learner:${{ matrix.buildType.dockerTag }} . -f paynt-learner.dockerfile --build-arg paynt_base=${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }} - name: Login into docker # Only login if using master on original repo (and not for pull requests or forks) if: github.repository_owner == 'randriu' && github.ref == 'refs/heads/master' @@ -62,7 +62,7 @@ jobs: - name: Build stormpy from Dockerfile run: docker build -t ${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }} . --build-arg STORM_BASE=movesrwth/storm:${{ matrix.buildType.stormTag }} --build-arg build_type=${{ matrix.buildType.buildArgs }} --build-arg setup_args=${{ matrix.buildType.setupArgs }} --build-arg setup_args_pycarl=${{ matrix.buildType.setupArgs }} --build-arg no_threads=${NR_JOBS} - name: Build image for learner - run: docker build -t ${{ matrix.buildType.imageName }}-learner:${{ matrix.buildType.dockerTag }} . -f paynt-learner.dockerfile --build-arg paynt-base=${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }} + run: docker build -t ${{ matrix.buildType.imageName }}-learner:${{ matrix.buildType.dockerTag }} . -f paynt-learner.dockerfile --build-arg paynt_base=${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }} - name: Login into docker # Only login if using master on original repo (and not for pull requests or forks) if: github.repository_owner == 'randriu' && github.ref == 'refs/heads/master' diff --git a/paynt-learner.dockerfile b/paynt-learner.dockerfile index ffa73da81..02eca0fb2 100644 --- a/paynt-learner.dockerfile +++ b/paynt-learner.dockerfile @@ -1,5 +1,5 @@ -ARG paynt-base=randriu/paynt:ci -FROM paynt-base +ARG paynt_base=randriu/paynt:ci +FROM $paynt_base RUN pip install torch --index-url https://download.pytorch.org/whl/cpu