Time Travelling #1468
Workflow file for this run
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Build Test | |
| # Builds and tests storm on various platforms | |
| # also deploys images to Dockerhub | |
| on: | |
| schedule: | |
| # run daily | |
| - cron: '0 6 * * *' | |
| # needed to trigger the workflow manually | |
| workflow_dispatch: | |
| pull_request: | |
| env: | |
| CARL_BRANCH: "master14" | |
| CARL_GIT_URL: "https://github.com/smtrat/carl.git" | |
| STORM_GIT_URL: "${{ github.server_url }}/${{ github.repository }}.git" | |
| STORM_BRANCH: "${{ github.ref }}" | |
| # github runners currently have two cores | |
| NR_JOBS: "2" | |
| # cmake arguments | |
| CMAKE_DEBUG: "-DCMAKE_BUILD_TYPE=Debug -DSTORM_DEVELOPER=ON -DSTORM_PORTABLE=ON -DSTORM_USE_SPOT_SHIPPED=ON" | |
| CMAKE_RELEASE: "-DCMAKE_BUILD_TYPE=Release -DSTORM_DEVELOPER=OFF -DSTORM_PORTABLE=ON -DSTORM_USE_SPOT_SHIPPED=ON" | |
| CARL_CMAKE_DEBUG: "-DCMAKE_BUILD_TYPE=Debug -DUSE_CLN_NUMBERS=ON -DUSE_GINAC=ON -DTHREAD_SAFE=ON" | |
| CARL_CMAKE_RELEASE: "-DCMAKE_BUILD_TYPE=Release -DUSE_CLN_NUMBERS=ON -DUSE_GINAC=ON -DTHREAD_SAFE=ON" | |
| jobs: | |
| indepthTests: | |
| name: Indepth Tests (${{ matrix.cmakeArgs.name }}) | |
| runs-on: ubuntu-latest | |
| env: | |
| DISTRO: "ubuntu-22.04" | |
| strategy: | |
| matrix: | |
| cmakeArgs: | |
| - {name: "GMP exact; GMP rational functions; Spot", args: "-DCMAKE_BUILD_TYPE=Debug -DSTORM_DEVELOPER=ON -DSTORM_PORTABLE=ON -DSTORM_USE_CLN_EA=OFF -DSTORM_USE_CLN_RF=OFF -DSTORM_USE_SPOT_SHIPPED=ON -DSTORM_COMPILE_WITH_ALL_SANITIZERS=ON"} | |
| # This is the standard config | |
| # - {name: "GMP exact; CLN rational functions; Spot", args: "-DCMAKE_BUILD_TYPE=Debug -DSTORM_DEVELOPER=ON -DSTORM_PORTABLE=ON -DSTORM_USE_CLN_EA=OFF -DSTORM_USE_CLN_RF=ON -DSTORM_USE_SPOT_SHIPPED=ON"} | |
| - {name: "CLN exact; GMP rational functions; Spot", args: "-DCMAKE_BUILD_TYPE=Debug -DSTORM_DEVELOPER=ON -DSTORM_PORTABLE=ON -DSTORM_USE_CLN_EA=ON -DSTORM_USE_CLN_RF=OFF -DSTORM_USE_SPOT_SHIPPED=ON -DSTORM_COMPILE_WITH_ALL_SANITIZERS=ON"} | |
| - {name: "CLN exact; CLN rational functions; Spot", args: "-DCMAKE_BUILD_TYPE=Debug -DSTORM_DEVELOPER=ON -DSTORM_PORTABLE=ON -DSTORM_USE_CLN_EA=ON -DSTORM_USE_CLN_RF=ON -DSTORM_USE_SPOT_SHIPPED=ON -DSTORM_COMPILE_WITH_ALL_SANITIZERS=ON"} | |
| - {name: "GMP exact; CLN rational functions; No Spot", args: "-DCMAKE_BUILD_TYPE=Debug -DSTORM_DEVELOPER=ON -DSTORM_PORTABLE=ON -DSTORM_USE_CLN_EA=OFF -DSTORM_USE_CLN_RF=ON -DSTORM_USE_SPOT_SHIPPED=OFF -DSTORM_COMPILE_WITH_ALL_SANITIZERS=ON"} | |
| steps: | |
| - name: Init Docker | |
| run: sudo docker run -d -it --name storm --privileged movesrwth/storm-basesystem:${DISTRO} | |
| - name: Git clone | |
| # git clone cannot clone individual commits based on a sha and some other refs | |
| # this workaround fixes this and fetches only one commit | |
| run: | | |
| sudo docker exec storm bash -c "mkdir /opt/storm; cd /opt/storm; git init && git remote add origin ${STORM_GIT_URL} && git fetch --depth 1 origin ${STORM_BRANCH} && git checkout FETCH_HEAD" | |
| - name: Run cmake | |
| run: sudo docker exec storm bash -c "mkdir /opt/storm/build; cd /opt/storm/build; cmake .. ${{ matrix.cmakeArgs.args }}" | |
| - name: Build storm | |
| run: sudo docker exec storm bash -c "cd /opt/storm/build; make -j ${NR_JOBS}" | |
| - name: Run unit tests | |
| run: sudo docker exec storm bash -c "cd /opt/storm/build; ASAN_OPTIONS=detect_leaks=0,detect_odr_violation=0 ctest test --output-on-failure" | |
| noDeploy: | |
| name: Build and Test | |
| runs-on: ubuntu-latest | |
| strategy: | |
| matrix: | |
| distro: ["debian-10", "debian-11", "ubuntu-18.04", "ubuntu-20.04"] | |
| debugOrRelease: ["release"] | |
| steps: | |
| - name: Setup cmake arguments | |
| # this is strangely the best way to implement environment variables based on the value of another | |
| # GITHUB_ENV is a magic variable pointing to a file; if a line with format {NAME}={VALUE} | |
| # then the env variable with name NAME will be created/updated with VALUE | |
| run: | | |
| ([[ ${{ matrix.debugOrRelease }} == "debug" ]] && echo "CMAKE_ARGS=${CMAKE_DEBUG}" || echo "CMAKE_ARGS=${CMAKE_RELEASE}") >> $GITHUB_ENV | |
| - name: Init Docker | |
| run: sudo docker run -d -it --name storm --privileged movesrwth/storm-basesystem:${{ matrix.distro }} | |
| - name: Git clone | |
| # git clone cannot clone individual commits based on a sha and some other refs | |
| # this workaround fixes this and fetches only one commit | |
| run: | | |
| sudo docker exec storm bash -c "mkdir /opt/storm; cd /opt/storm; git init && git remote add origin ${STORM_GIT_URL} && git fetch --depth 1 origin ${STORM_BRANCH} && git checkout FETCH_HEAD" | |
| - name: Run cmake | |
| run: sudo docker exec storm bash -c "mkdir /opt/storm/build; cd /opt/storm/build; cmake .. ${CMAKE_ARGS}" | |
| - name: Build storm | |
| run: sudo docker exec storm bash -c "cd /opt/storm/build; make -j ${NR_JOBS}" | |
| # A bit hacky... but its usefullnes has been proven in production | |
| - name: Check release makeflags | |
| if: matrix.debugOrRelease == 'release' | |
| run: | | |
| sudo docker exec storm bash -c "/opt/storm/build/bin/storm --version | grep 'with flags .* -O3' || (echo \"Error: Missing flag \'-O3\' for release build.\" && false)" | |
| sudo docker exec storm bash -c "/opt/storm/build/bin/storm --version | grep 'with flags .* -DNDEBUG' || (echo \"Error: Missing flag \'-DNDEBUG\' for release build.\" && false)" | |
| - name: Check debug makeflags | |
| if: matrix.debugOrRelease == 'debug' | |
| run: | | |
| sudo docker exec storm bash -c "/opt/storm/build/bin/storm --version | grep 'with flags .* -g' || (echo \"Error: Missing flag \'-g\' for debug build.\" && false)" | |
| - name: Run unit tests | |
| run: sudo docker exec storm bash -c "cd /opt/storm/build; ctest test --output-on-failure" | |
| deploy: | |
| name: Build, Test and Deploy | |
| runs-on: ubuntu-latest | |
| env: | |
| DISTRO: "ubuntu-22.04" | |
| strategy: | |
| matrix: | |
| debugOrRelease: ["debug", "release"] | |
| steps: | |
| - name: Setup cmake arguments | |
| # this is strangely the best way to implement environment variables based on the value of another | |
| # GITHUB_ENV is a magic variable pointing to a file; if a line with format {NAME}={VALUE} | |
| # then the env variable with name NAME will be created/updated with VALUE | |
| run: | | |
| ([[ ${{ matrix.debugOrRelease }} == "debug" ]] && echo "CMAKE_ARGS=${CMAKE_DEBUG}" || echo "CMAKE_ARGS=${CMAKE_RELEASE}") >> $GITHUB_ENV | |
| ([[ ${{ matrix.debugOrRelease }} == "debug" ]] && echo "CARL_CMAKE_ARGS=${CARL_CMAKE_DEBUG}" || echo "CARL_CMAKE_ARGS=${CARL_CMAKE_RELEASE}") >> $GITHUB_ENV | |
| - name: Login into docker | |
| # Only login if using master on original repo (and not for pull requests or forks) | |
| if: github.repository_owner == 'moves-rwth' && github.ref == 'refs/heads/master' | |
| run: echo "${{ secrets.STORM_CI_DOCKER_PASSWORD }}" | sudo docker login -u "${{ secrets.STORM_CI_DOCKER_USERNAME }}" --password-stdin | |
| - name: Init Docker | |
| run: sudo docker run -d -it --name storm --privileged movesrwth/storm-basesystem:${DISTRO} | |
| ##### | |
| # Build & DEPLOY CARL | |
| ##### | |
| # We should not do partial updates :/ | |
| # but we need to install some dependencies | |
| # Surely we can find a better way to do this at some point | |
| - name: Update base system | |
| run: | | |
| sudo docker exec storm apt-get update | |
| sudo docker exec storm apt-get upgrade -qqy | |
| - name: install dependencies | |
| run: sudo docker exec storm apt-get install -qq -y uuid-dev pkg-config | |
| - name: Git clone carl | |
| run: sudo docker exec storm git clone --depth 1 --branch $CARL_BRANCH $CARL_GIT_URL /opt/carl | |
| - name: Run cmake for carl | |
| run: sudo docker exec storm bash -c "mkdir /opt/carl/build; cd /opt/carl/build; cmake .. ${CARL_CMAKE_ARGS}" | |
| - name: Build carl | |
| run: sudo docker exec storm bash -c "cd /opt/carl/build; make lib_carl -j ${NR_JOBS}" | |
| - name: Deploy carl | |
| # Only deploy if using master on original repo (and not for pull requests or forks) | |
| if: github.repository_owner == 'moves-rwth' && github.ref == 'refs/heads/master' | |
| run: | | |
| sudo docker commit storm movesrwth/carl:ci-${{ matrix.debugOrRelease }} | |
| sudo docker push movesrwth/carl:ci-${{ matrix.debugOrRelease }} | |
| ##### | |
| # Build & TEST & DEPLOY STORM | |
| ##### | |
| - name: Git shallow clone | |
| # Only clone shallow if not using master on original repo (and not for pull requests or forks) | |
| if: ${{ !(github.repository_owner == 'moves-rwth' && github.ref == 'refs/heads/master') }} | |
| run: | | |
| # git clone cannot clone individual commits based on a sha and some other refs | |
| sudo docker exec storm bash -c "mkdir /opt/storm; cd /opt/storm; git init && git remote add origin ${STORM_GIT_URL} && git fetch --depth 1 origin ${STORM_BRANCH} && git checkout FETCH_HEAD" | |
| - name: Git deep clone | |
| # needed for versioning for now on deployment | |
| if: github.repository_owner == 'moves-rwth' && github.ref == 'refs/heads/master' | |
| run: | | |
| sudo docker exec storm git clone --branch master $STORM_GIT_URL /opt/storm | |
| - name: Run cmake | |
| run: sudo docker exec storm bash -c "mkdir /opt/storm/build; cd /opt/storm/build; cmake .. ${CMAKE_ARGS}" | |
| - name: Build storm | |
| run: sudo docker exec storm bash -c "cd /opt/storm/build; make -j ${NR_JOBS}" | |
| # A bit hacky... but its usefulness has been proven in production | |
| - name: Check release makeflags | |
| if: matrix.debugOrRelease == 'release' | |
| run: | | |
| sudo docker exec storm bash -c "/opt/storm/build/bin/storm --version | grep 'with flags .* -O3' || (echo \"Error: Missing flag \'-O3\' for release build.\" && false)" | |
| sudo docker exec storm bash -c "/opt/storm/build/bin/storm --version | grep 'with flags .* -DNDEBUG' || (echo \"Error: Missing flag \'-DNDEBUG\' for release build.\" && false)" | |
| - name: Check debug makeflags | |
| if: matrix.debugOrRelease == 'debug' | |
| run: | | |
| sudo docker exec storm bash -c "/opt/storm/build/bin/storm --version | grep 'with flags .* -g' || (echo \"Error: Missing flag \'-g\' for debug build.\" && false)" | |
| - name: Run unit tests | |
| run: sudo docker exec storm bash -c "cd /opt/storm/build; ctest test --output-on-failure" | |
| - name: Deploy storm | |
| # Only deploy if using master on original repo (and not for pull requests or forks) | |
| if: github.repository_owner == 'moves-rwth' && github.ref == 'refs/heads/master' | |
| run: | | |
| sudo docker commit storm movesrwth/storm:ci-${{ matrix.debugOrRelease }} | |
| sudo docker push movesrwth/storm:ci-${{ matrix.debugOrRelease }} | |
| notify: | |
| name: Email notification | |
| runs-on: ubuntu-latest | |
| needs: [indepthTests, noDeploy, deploy] | |
| # Only run in main repo and even if previous step failed | |
| if: github.repository_owner == 'moves-rwth' && always() | |
| steps: | |
| - uses: technote-space/workflow-conclusion-action@v2 | |
| - uses: dawidd6/action-send-mail@v2 | |
| with: | |
| server_address: ${{ secrets.STORM_CI_MAIL_SERVER }} | |
| server_port: 587 | |
| username: ${{ secrets.STORM_CI_MAIL_USERNAME }} | |
| password: ${{ secrets.STORM_CI_MAIL_PASSWORD }} | |
| subject: "[You broke it] CI run failed for ${{ github.repository }}" | |
| body: | |
| "CI job of ${{ github.repository }} has failed for commit ${{ github.sha }}.\n\ | |
| The error type is: ${{ env.WORKFLOW_CONCLUSION }}.\n\n\ | |
| For more information, see https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}" | |
| to: ${{ secrets.STORM_CI_MAIL_RECIPIENTS }} | |
| from: Github Actions <[email protected]> | |
| if: env.WORKFLOW_CONCLUSION != 'success' # notify only if failure |