diff --git a/.github/workflows/Dockerfile.archlinux b/.github/workflows/Dockerfile.archlinux index 9e6312e2f4..284d4cdeb3 100644 --- a/.github/workflows/Dockerfile.archlinux +++ b/.github/workflows/Dockerfile.archlinux @@ -1,14 +1,21 @@ -# Base Dockerfile for using Storm on Archlinux -############################################## +# Dockerfile for Storm on Archlinux +################################### # The Docker image can be built by executing: # docker build -t yourusername/storm . +# A different base image can be set from the commandline with: +# --build-arg BASE_IMAGE= -FROM archlinux:latest -MAINTAINER Matthias Volk +# Set base image +ARG BASE_IMAGE=archlinux:latest +FROM $BASE_IMAGE +LABEL org.opencontainers.image.authors="dev@stormchecker.org" + + +# Configuration arguments +######################### +# The arguments can be set from the commandline with: +# --build-arg = -# Specify configurations -# These configurations can be set from the commandline with: -# --build-arg = # CMake build type ARG build_type=Release # Specify number of threads to use for parallel compilation @@ -29,6 +36,7 @@ ARG cmake_args="" # Additional Archlinux packages ARG packages="" + # Install dependencies ###################### RUN pacman -Syu --noconfirm # Updates needed as Archlinux is rolling release diff --git a/.github/workflows/Dockerfile.doxygen b/.github/workflows/Dockerfile.doxygen index 749bce87a2..58005074a2 100644 --- a/.github/workflows/Dockerfile.doxygen +++ b/.github/workflows/Dockerfile.doxygen @@ -2,14 +2,20 @@ ############################################## # The Docker image can be built by executing: # docker build -t yourusername/storm . +# A different base image can be set from the commandline with: +# --build-arg BASE_IMAGE= # Set base image -FROM movesrwth/storm-dependencies:latest -MAINTAINER Matthias Volk +ARG BASE_IMAGE=movesrwth/storm-dependencies:latest +FROM $BASE_IMAGE +LABEL org.opencontainers.image.authors="dev@stormchecker.org" + + +# Configuration arguments +######################### +# The arguments can be set from the commandline with: +# --build-arg = -# Specify configurations -# These configurations can be set from the commandline with: -# --build-arg = # Specify number of threads to use for parallel compilation ARG no_threads=1 diff --git a/.github/workflows/buildtest.yml b/.github/workflows/buildtest.yml index de8d2b546a..37be2be133 100644 --- a/.github/workflows/buildtest.yml +++ b/.github/workflows/buildtest.yml @@ -4,8 +4,8 @@ name: Build Test on: schedule: - # run daily - - cron: '0 6 * * *' + # run daily + - cron: '0 6 * * *' # needed to trigger the workflow manually workflow_dispatch: pull_request: @@ -88,7 +88,7 @@ jobs: - name: Build storm from Dockerfile run: | docker build -t movesrwth/storm:ci . \ - --build-arg BASE_IMG=movesrwth/${{ matrix.config.baseImg }} \ + --build-arg BASE_IMAGE=movesrwth/${{ matrix.config.baseImg }} \ --build-arg build_type="${{ matrix.config.buildType }}" \ --build-arg gurobi_support="${{ matrix.config.Gurobi }}" \ --build-arg soplex_support="${{ matrix.config.Soplex }}" \ @@ -193,7 +193,7 @@ jobs: - name: Build storm from Dockerfile run: | docker build -t movesrwth/storm:ci . \ - --build-arg BASE_IMG=movesrwth/storm-basesystem:${{ matrix.distro }} \ + --build-arg BASE_IMAGE=movesrwth/storm-basesystem:${{ matrix.distro }} \ --build-arg build_type="${{ matrix.buildType }}" \ --build-arg gurobi_support="OFF" \ --build-arg soplex_support="OFF" \ @@ -220,26 +220,25 @@ jobs: run: docker exec ci bash -c "cd /opt/storm/build; ctest test --output-on-failure" macTests: - name: macOS Tests (${{ matrix.config.name }}) + name: macOS Tests (${{ matrix.config.name }}, ${{ matrix.config.buildType }}) strategy: matrix: config: - - {name: "XCode 14.3, Intel, Release", + - {name: "XCode 14.3, Intel", distro: "macos-13", xcode: "14.3", - buildType: "Release" + buildType: "Debug" } - - {name: "XCode 15.4, ARM, Release", + - {name: "XCode 15.4, ARM", distro: "macos-14", xcode: "15.4", - buildType: "Release" + buildType: "Debug" } - - {name: "XCode 16.3, ARM, Release", + - {name: "XCode 16.3, ARM", distro: "macos-15", xcode: "16.3", - buildType: "Release" + buildType: "Debug" } - buildType: ["Release"] runs-on: ${{ matrix.config.distro }} steps: - uses: maxim-lobanov/setup-xcode@v1 @@ -281,6 +280,7 @@ jobs: working-directory: ./build run: ctest test--output-on-failure + deploy: name: Test and Deploy (${{ matrix.buildType.name }}) runs-on: ubuntu-latest @@ -308,7 +308,7 @@ jobs: - name: Build storm from Dockerfile run: | docker build -t movesrwth/storm:${{ matrix.buildType.dockerTag }} . \ - --build-arg BASE_IMG=movesrwth/${{ matrix.buildType.baseImg }} \ + --build-arg BASE_IMAGE=movesrwth/${{ matrix.buildType.baseImg }} \ --build-arg build_type="${{ matrix.buildType.name }}" \ --build-arg developer="${{ matrix.buildType.Developer }}" \ --build-arg cmake_args="${{ matrix.buildType.cmakeArgs }}" \ @@ -336,7 +336,10 @@ jobs: - 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 }}" | docker login -u "${{ secrets.STORM_CI_DOCKER_USERNAME }}" --password-stdin + uses: docker/login-action@v3 + with: + username: ${{ secrets.STORM_CI_DOCKER_USERNAME }} + password: ${{ secrets.STORM_CI_DOCKER_TOKEN }} - 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' diff --git a/.github/workflows/formatapply.yml b/.github/workflows/formatapply.yml index ad8b745073..1198dcea07 100644 --- a/.github/workflows/formatapply.yml +++ b/.github/workflows/formatapply.yml @@ -1,6 +1,7 @@ -name: apply-code-format +name: Apply code format -on: [ workflow_dispatch ] +on: + workflow_dispatch: jobs: build: diff --git a/.github/workflows/formatcheck.yml b/.github/workflows/formatcheck.yml index 0fb4d54bdf..1ac9b74ce1 100644 --- a/.github/workflows/formatcheck.yml +++ b/.github/workflows/formatcheck.yml @@ -1,6 +1,9 @@ -name: check-code-format +name: Check code format -on: [push, pull_request, workflow_dispatch] +on: + push: + pull_request: + workflow_dispatch: jobs: build: diff --git a/.github/workflows/release_docker.yml b/.github/workflows/release_docker.yml index 18f1178f09..28ca54c333 100644 --- a/.github/workflows/release_docker.yml +++ b/.github/workflows/release_docker.yml @@ -1,7 +1,10 @@ name: Release Docker -# Builds and deploys images to Dockerhub +# Builds Storm and deploys images to Dockerhub +# Build is distributed across multiple runners based on: +# https://docs.docker.com/build/ci/github-actions/multi-platform/#distribute-build-across-multiple-runners -on: +on: + # needed to trigger the workflow manually workflow_dispatch: inputs: tag: @@ -10,36 +13,49 @@ on: default: 'x.y.z' env: + IMAGE: movesrwth/storm # GitHub runners currently have 4 cores NR_JOBS: "4" jobs: - deploy: - name: Deploy (${{ matrix.buildType.name }}) - runs-on: ubuntu-latest + build: + name: Build ${{ matrix.image.tag }} on ${{ matrix.platform.name }} + runs-on: ${{ matrix.platform.runner }} strategy: matrix: - buildType: - - {name: "Debug", - suffix: "-debug", - Developer: "ON" + image: + - {tag: "${{ github.event.inputs.tag }}-debug", + baseImg: "movesrwth/storm-dependencies:latest-debug", + file: "Dockerfile", + buildType: "Debug", + developer: "ON" } - - {name: "Release", - suffix: "", - Developer: "OFF" + - {tag: "${{ github.event.inputs.tag }}", + baseImg: "movesrwth/storm-dependencies:latest", + file: "Dockerfile", + buildType: "Release", + developer: "OFF" } + platform: + - {name: linux/amd64, runner: "ubuntu-latest"} + - {name: linux/arm64, runner: "ubuntu-24.04-arm"} steps: - name: Git clone uses: actions/checkout@v4 - - name: Build storm from Dockerfile + - name: Prepare + # Sanitize platform name run: | - docker build -t movesrwth/storm:${{ github.event.inputs.tag }}${{ matrix.buildType.suffix }} . \ - --build-arg BASE_IMG=movesrwth/storm-dependencies:latest${{ matrix.buildType.suffix }} \ - --build-arg build_type="${{ matrix.buildType.name }}" \ - --build-arg developer="${{ matrix.buildType.Developer }}" \ - --build-arg cmake_args="${{ matrix.buildType.cmakeArgs }}" \ - --build-arg no_threads=${NR_JOBS} - # Omitting arguments gurobi_support, soplex_support, spot_support, cln_exact, cln_ratfunc, all_sanitizers + platform=${{ matrix.platform.name }} + echo "PLATFORM=${platform//\//-}" >> $GITHUB_ENV + - name: Docker metadata + id: meta + uses: docker/metadata-action@v5 + with: + images: ${{ env.IMAGE }} + tags: | + type=raw,${{ matrix.image.tag }} + - name: Set up Docker Buildx + uses: docker/setup-buildx-action@v3 - name: Login to Docker Hub # Only login if using original repo if: github.repository_owner == 'moves-rwth' @@ -47,8 +63,73 @@ jobs: with: username: ${{ secrets.STORM_CI_DOCKER_USERNAME }} password: ${{ secrets.STORM_CI_DOCKER_TOKEN }} - - name: Deploy storm - # Only deploy if using original repo + - name: Build and push by digest + id: build + uses: docker/build-push-action@v6 + with: + file: ${{ matrix.image.file }} + # Set build arguments + build-args: | + BASE_IMAGE=${{ matrix.image.baseImg }} + build_type=${{ matrix.image.buildType }} + developer=${{ matrix.image.developer }} + no_threads=${{ env.NR_JOBS }} + # Omitting arguments cmake_args, gurobi_support, soplex_support, spot_support, cln_exact, cln_ratfunc, all_sanitizers + platforms: ${{ matrix.platform.name }} + labels: ${{ steps.meta.outputs.labels }} + outputs: type=image,name=${{ env.IMAGE }},push-by-digest=true,name-canonical=true,push=true + - name: Export digest + run: | + mkdir -p ${{ runner.temp }}/digests/${{ matrix.image.tag }} + digest="${{ steps.build.outputs.digest }}" + touch "${{ runner.temp }}/digests/${{ matrix.image.tag }}/${digest#sha256:}" + - name: Upload digest + uses: actions/upload-artifact@v4 + with: + name: ${{ matrix.image.tag }}-digests-${{ env.PLATFORM }} + path: ${{ runner.temp }}/digests/${{ matrix.image.tag }}/* + if-no-files-found: error + retention-days: 1 + + merge: + name: Merge manifests for ${{ matrix.image.tag }} + runs-on: ubuntu-latest + needs: + - build + strategy: + matrix: + image: + # Must be the same as above + - {tag: "${{ github.event.inputs.tag }}-debug"} + - {tag: "${{ github.event.inputs.tag }}"} + steps: + - name: Download digests + uses: actions/download-artifact@v4 + with: + path: ${{ runner.temp }}/digests/${{ matrix.image.tag }} + pattern: ${{ matrix.image.tag }}-digests-* + merge-multiple: true + - name: Set up Docker Buildx + uses: docker/setup-buildx-action@v3 + - name: Docker metadata + id: meta + uses: docker/metadata-action@v5 + with: + images: ${{ env.IMAGE }} + tags: | + type=raw,${{ matrix.image.tag }} + - name: Login to Docker Hub + # Only login if using original repo if: github.repository_owner == 'moves-rwth' + uses: docker/login-action@v3 + with: + username: ${{ secrets.STORM_CI_DOCKER_USERNAME }} + password: ${{ secrets.STORM_CI_DOCKER_TOKEN }} + - name: Create manifest list and push + working-directory: ${{ runner.temp }}/digests/${{ matrix.image.tag }} + run: | + docker buildx imagetools create $(jq -cr '.tags | map("-t " + .) | join(" ")' <<< '${{ steps.meta.outputs.json}}') \ + $(printf '${{ env.IMAGE }}@sha256:%s ' *) + - name: Inspect image run: | - docker push movesrwth/storm:${{ github.event.inputs.tag }}${{ matrix.buildType.suffix }} + docker buildx imagetools inspect ${{ env.IMAGE }}:${{ steps.meta.outputs.version }} diff --git a/Dockerfile b/Dockerfile index b08afb16c3..25a5bd0ef7 100644 --- a/Dockerfile +++ b/Dockerfile @@ -1,19 +1,21 @@ -# Base Dockerfile for using Storm -################################# +# Dockerfile for Storm +###################### # The Docker image can be built by executing: # docker build -t yourusername/storm . # A different base image can be set from the commandline with: -# --build-arg BASE_IMG= +# --build-arg BASE_IMAGE= # Set base image -ARG BASE_IMG=movesrwth/storm-dependencies:latest -ARG BASE_PLATFORM=linux/amd64 -FROM --platform=$BASE_PLATFORM $BASE_IMG -MAINTAINER Matthias Volk +ARG BASE_IMAGE=movesrwth/storm-dependencies:latest +FROM $BASE_IMAGE +LABEL org.opencontainers.image.authors="dev@stormchecker.org" + + +# Configuration arguments +######################### +# The arguments can be set from the commandline with: +# --build-arg = -# Specify configurations -# These configurations can be set from the commandline with: -# --build-arg = # CMake build type ARG build_type=Release # Specify number of threads to use for parallel compilation diff --git a/doc/scripts/test_build_configurations.py b/doc/scripts/test_build_configurations.py deleted file mode 100644 index 56baccf0df..0000000000 --- a/doc/scripts/test_build_configurations.py +++ /dev/null @@ -1,118 +0,0 @@ -import subprocess -import os -import shutil -import time -import math -import sys - -logfileDir = "test_build_configurations_logs" -pathToConfigFile = "" -globalCmakeArguments = "" -globalMakeArguments = "" - -if len(sys.argv) == 1 or len(sys.argv) > 5: - print "Usage: " + sys.argv[0] + "/path/to/storm /path/to/configurations.txt \"optional make arguments\" \"optional cmake arguments\"" - print "Example: " + sys.argv[0] + " ~/storm test_build_configurations.txt \"-j 48 -k\" \"-DZ3_ROOT=/path/to/z3/\"" - sys.exit(0) - -pathToStorm = sys.argv[1] -pathToConfigFile = sys.argv[2] - -if len(sys.argv) > 3: - globalMakeArguments = sys.argv[3] - print globalMakeArguments -if len(sys.argv) > 4: - globalCmakeArguments = sys.argv[4] - print globalCmakeArguments - -# create directory for log files -if not os.path.exists(logfileDir): - os.makedirs(logfileDir) - -unsuccessfulConfigs = "" -globalStartTime = time.time() - -with open(pathToConfigFile) as configfile: - localStartTime = time.time() - configId=0 - for localCmakeArguments in configfile: - - cmakeArguments = globalCmakeArguments + " " + localCmakeArguments.strip('\n') - buildDir = os.path.join(pathToStorm, "build{}".format(configId)) - logfilename = os.path.join(logfileDir, "build{}".format(configId) + "_" + time.strftime("%Y-%m-%d-%H-%M-%S") + ".log") - - - print "Building configuration {} with cmake options ".format(configId) + cmakeArguments - print "\tCreating log file " + logfilename + " ..." - with open(logfilename, "w") as logfile: - success=True - logfile.write("Log for test configuration " + cmakeArguments + "\n") - - print "\tCreating build directory" + buildDir + " ..." - if os.path.exists(buildDir): - print "\t\tRemoving existing directory " + buildDir - shutil.rmtree(buildDir, ignore_errors=True) - os.makedirs(buildDir) - logfile.write("Build directory is " + buildDir + "\n") - print "\t\tdone" - - if success: - print "\tInvoking cmake ..." - cmakeCommand = "cmake .. {}".format(cmakeArguments) - logfile.write ("\n\n CALLING CMAKE \n\n" + cmakeCommand + "\n") - try: - cmakeOutput = subprocess.check_output("cd " + buildDir + "; " + cmakeCommand , shell=True,stderr=subprocess.STDOUT) - print "\t\tdone" - logfile.write(cmakeOutput) - except subprocess.CalledProcessError as e: - success=False - print "\t\tfail" - print e.output - logfile.write(e.output) - - if success: - print "\tInvoking make ..." - makeCommand = "make {}".format(globalMakeArguments) - logfile.write ("\n\n CALLING MAKE \n\n" + makeCommand + "\n") - try: - makeOutput = subprocess.check_output("cd " + buildDir + "; " + makeCommand , shell=True,stderr=subprocess.STDOUT) - print "\t\tdone" - logfile.write(makeOutput) - except subprocess.CalledProcessError as e: - success=False - print "\t\tfail" - print e.output - logfile.write(e.output) - - if success: - print "\tInvoking make check..." - makeCheckCommand = "make check" - logfile.write ("\n\n CALLING MAKE CHECK \n\n" + makeCheckCommand + "\n") - try: - makeCheckOutput = subprocess.check_output("cd " + buildDir + "; " + makeCheckCommand , shell=True,stderr=subprocess.STDOUT) - print "\t\tdone" - logfile.write(makeCheckOutput) - except subprocess.CalledProcessError as e: - success=False - print "\t\tfail" - print e.output - logfile.write(e.output) - - localEndTime = time.time() - if success: - print "\tConfiguration build and tested successfully within {} minutes.".format(int((localEndTime - localStartTime)/60)) - else: - print "\tAn error occurred for this configuration." - unsuccessfulConfigs += buildDir + " with arguments " + cmakeArguments + "\n" - - configId += 1 -globalEndTime = time.time() -print "All tests completed after {} minutes.".format(int((globalEndTime - globalStartTime)/60)) -if unsuccessfulConfigs == "": - print "All configurations were build and tested successfully." -else: - print "The following configurations failed: \n" + unsuccessfulConfigs - - - - diff --git a/doc/scripts/test_build_configurations.txt b/doc/scripts/test_build_configurations.txt deleted file mode 100644 index 3688e8eab0..0000000000 --- a/doc/scripts/test_build_configurations.txt +++ /dev/null @@ -1,5 +0,0 @@ --DSTORM_USE_CLN_EA=OFF -DSTORM_USE_CLN_RF=OFF --DSTORM_USE_CLN_EA=OFF -DSTORM_USE_CLN_RF=ON --DSTORM_USE_CLN_EA=ON -DSTORM_USE_CLN_RF=OFF --DSTORM_USE_CLN_EA=ON -DSTORM_USE_CLN_RF=ON --DCMAKE_BUILD_TYPE=DEBUG -DSTORM_DEVELOPER=ON \ No newline at end of file