You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
210 lines
12 KiB
210 lines
12 KiB
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 -DBUILD_ADDONS=ON -DBUILD_ADDON_PARSER=ON"
|
|
CARL_CMAKE_RELEASE: "-DCMAKE_BUILD_TYPE=Release -DUSE_CLN_NUMBERS=ON -DUSE_GINAC=ON -DTHREAD_SAFE=ON -DBUILD_ADDONS=ON -DBUILD_ADDON_PARSER=ON"
|
|
|
|
|
|
jobs:
|
|
indepthTests:
|
|
name: Indepth Tests (${{ matrix.cmakeArgs.name }})
|
|
runs-on: ubuntu-latest
|
|
env:
|
|
DISTRO: "ubuntu-20.10"
|
|
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"}
|
|
# 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"}
|
|
- {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"}
|
|
- {name: "GMP exact; CLN rational functions; No 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=OFF"}
|
|
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; ctest test --output-on-failure"
|
|
|
|
noDeploy:
|
|
name: Build and Test
|
|
runs-on: ubuntu-latest
|
|
strategy:
|
|
matrix:
|
|
distro: ["ubuntu-18.04", "debian-10", "debian-9", "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-20.10"
|
|
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 <you-broke-it@stormchecker.org>
|
|
if: env.WORKFLOW_CONCLUSION != 'success' # notify only if failure
|