Build a truly multi platform docker image

.github/workflows/docker.yml

@@ -5,7 +5,7 @@ on:
     - cron: '30 18 * * *'
 
 env:
-  CERBERUS_IMAGE_ID: ghcr.io/rems-project/cerberus/cn:release
+  CERBERUS_IMAGE_ID: ghcr.io/rems-project/cerberus/cn
 
 # Cancelling an in-progress job when a new push is performed causes the CI to
 # show up as failed: https://github.com/orgs/community/discussions/8336
@@ -15,12 +15,10 @@ concurrency:
   group: docker-${{ github.workflow }}-${{ github.ref }}
   cancel-in-progress: false
 
+# Instructions from https://depot.dev/blog/multi-platform-docker-images-in-github-actions
 jobs:
-  deploy-docker:
+  docker-release-ubuntu:
     runs-on: ubuntu-latest
-    strategy:
-      matrix:
-        platform: [linux/amd64, linux/arm64]
     permissions:
       packages: write
       contents: read
@@ -40,11 +38,47 @@ jobs:
       uses: docker/setup-qemu-action@v3
     - name: Set up Docker Buildx
       uses: docker/setup-buildx-action@v3
-    - name: Build the Docker image
-      run: |
-        echo "Building ${{env.CERBERUS_IMAGE_ID}}"
-        PLATFORM=${{ matrix.platform }} make -f Makefile_docker release_cn
-        docker tag cn:release ${{env.CERBERUS_IMAGE_ID}}
-
-    - name: Push the Docker image
-      run: docker push ${{env.CERBERUS_IMAGE_ID}}
+
+    - name: Build multi-platform image
+      uses: docker/build-push-action@v5
+      with:
+        context: .
+        platforms: linux/amd64,linux/arm64
+        push: true
+        tags: ${{env.CERBERUS_IMAGE_ID}}:release
+        file: Dockerfile.ubuntu
+        github-token: ${{ secrets.GITHUB_TOKEN }}
+
+  docker-release-redhat:
+    runs-on: ubuntu-latest
+    permissions:
+      packages: write
+      contents: read
+      attestations: write
+      id-token: write
+    steps:
+    - uses: actions/checkout@v4
+
+    - name: Login to GitHub Container Registry
+      uses: docker/login-action@v3
+      with:
+        registry: ghcr.io
+        username: ${{ github.actor }}
+        password: ${{ secrets.GITHUB_TOKEN }}
+
+    - name: Set up QEMU
+      uses: docker/setup-qemu-action@v3
+    - name: Set up Docker Buildx
+      uses: docker/setup-buildx-action@v3
+
+    - name: Build multi-platform image
+      uses: docker/build-push-action@v5
+      with:
+        context: .
+        platforms: linux/amd64,linux/arm64
+        push: true
+        tags: ${{env.CERBERUS_IMAGE_ID}}:release-redhat
+        file: Dockerfile.redhat
+        attests: type=sbom
+        provenance: mode=max
+        github-token: ${{ secrets.GITHUB_TOKEN }}

Dockerfile.redhat

@@ -0,0 +1,38 @@
+FROM redhat/ubi9:latest
+
+# Install basic dependencies
+RUN yum update -y && \
+    yum install -y xz sudo gcc unzip \
+    diffutils patch pkgconfig bzip2 \
+    git perl wget ca-certificates \
+    mpfr-devel gmp-devel m4
+
+# Install additional FEDORA packages
+# from https://www.cyberciti.biz/faq/install-epel-repo-on-an-rhel-8-x/
+# Currently the FEDORA packages are needed only for Z3
+# NOTE: we might have to eventually use *only* RedHat packages
+# which would mean installing Z3 directly from the release page
+RUN yum install -y https://dl.fedoraproject.org/pub/epel/epel-release-latest-9.noarch.rpm && \
+    yum update -y && \
+    yum install -y z3
+
+# Install OPAM
+# See https://opam.ocaml.org/doc/1.2/Install.html
+RUN curl -fsSL https://opam.ocaml.org/install.sh | sh
+
+ENV OPAMCONFIRMLEVEL=unsafe-yes
+RUN opam init --disable-sandboxing
+
+ADD . /opt/cerberus
+WORKDIR /opt/cerberus
+RUN opam install --deps-only  ./cerberus-lib.opam ./cn.opam
+
+RUN eval `opam env` \
+  && make install_cn
+
+WORKDIR /opt
+
+COPY docker_entry_point.sh /opt/docker_entry_point.sh
+RUN chmod +x /opt/docker_entry_point.sh
+WORKDIR /data
+ENTRYPOINT ["/opt/docker_entry_point.sh"]

Dockerfile.deps → Dockerfile.ubuntu

@@ -1,3 +1,4 @@
+# Build a minimal release image
 FROM ubuntu:22.04
 
 RUN apt-get update
@@ -6,13 +7,17 @@ RUN apt-get install -y opam libgmp-dev libmpfr-dev
 
 ENV OPAMCONFIRMLEVEL=unsafe-yes
 RUN opam init --disable-sandboxing
-RUN opam install dune lem
 
 ADD . /opt/cerberus
 WORKDIR /opt/cerberus
 RUN opam install --deps-only  ./cerberus-lib.opam ./cn.opam
+
 RUN eval `opam env` \
-  && make install \
   && make install_cn
 
-WORKDIR /opt
+WORKDIR /opt
+
+COPY docker_entry_point.sh /opt/docker_entry_point.sh
+RUN chmod +x /opt/docker_entry_point.sh
+WORKDIR /data
+ENTRYPOINT ["/opt/docker_entry_point.sh"]

README.md

@@ -1,6 +1,6 @@
 # Cerberus C semantics
 
-[![CI](https://github.com/rems-project/cerberus/actions/workflows/ci.yml/badge.svg)](https://github.com/rems-project/cerberus/actions/workflows/ci.yml)
+[![CI](https://github.com/rems-project/cerberus/actions/workflows/ci.yml/badge.svg)](https://github.com/rems-project/cerberus/actions/workflows/ci.yml) [![CI-CN](https://github.com/rems-project/cerberus/actions/workflows/ci-cn.yml/badge.svg)](https://github.com/rems-project/cerberus/actions/workflows/ci-cn.yml) [![CI-CN-specs-testing](https://github.com/rems-project/cerberus/actions/workflows/ci-cn-spec-testing.yml/badge.svg)](https://github.com/rems-project/cerberus/actions/workflows/ci-cn-spec-testing.yml) [![CI-CN-becnhmarks](https://github.com/rems-project/cerberus/actions/workflows/ci-cn-bench.yml/badge.svg)](https://github.com/rems-project/cerberus/actions/workflows/ci-cn-bench.yml) [![CI-CHERI](https://github.com/rems-project/cerberus/actions/workflows/ci-cheri.yml/badge.svg)](https://github.com/rems-project/cerberus/actions/workflows/ci-cheri.yml) [![Docker](https://github.com/rems-project/cerberus/actions/workflows/docker.yml/badge.svg)](https://github.com/rems-project/cerberus/actions/workflows/docker.yml)
 
 
 Web interfaces, papers, and web page