diff --git a/.github/workflows/docker.yml b/.github/workflows/docker.yml index f872e0a3c..d706c6f08 100644 --- a/.github/workflows/docker.yml +++ b/.github/workflows/docker.yml @@ -82,3 +82,16 @@ jobs: attests: type=sbom provenance: mode=max github-token: ${{ secrets.GITHUB_TOKEN }} + + test-docker-images: + runs-on: ubuntu-latest + strategy: + matrix: + tag: [release, release-redhat] + steps: + - uses: actions/checkout@v4 + + - name: Run CN CI tests + run: | + docker pull ${{env.CERBERUS_IMAGE_ID}}:${{ matrix.tag }} + docker run -v $PWD:/work ${{env.CERBERUS_IMAGE_ID}}:${{ matrix.tag }} tests/run-cn.sh diff --git a/Dockerfile.ubuntu b/Dockerfile.ubuntu index 4fe361313..26657ef57 100644 --- a/Dockerfile.ubuntu +++ b/Dockerfile.ubuntu @@ -11,6 +11,7 @@ RUN opam init --disable-sandboxing ADD . /opt/cerberus WORKDIR /opt/cerberus RUN opam install --deps-only ./cerberus-lib.opam ./cn.opam +RUN opam install z3 RUN eval `opam env` \ && make install_cn diff --git a/README.md b/README.md index ab6ccfde2..28c2991a5 100644 --- a/README.md +++ b/README.md @@ -183,10 +183,22 @@ See https://github.com/rems-project/cerberus/blob/master/backend/cn/README.md Docker image ------------ +A pre-build docker image with `cerberus` and `cn` can be downloaded with: + +* For the Ubuntu 22.04 based image (recommended): + ```bash + $ docker pull ghcr.io/rems-project/cerberus/cn:release + ``` +* For Redhat Ubi9 based image: + ```bash + $ docker pull ghcr.io/rems-project/cerberus/cn:release-redhat + ``` + +For a local build, run: ```bash -$ make -f Makefile_docker +$ docker build -t cn:release -f Dockerfile.ubuntu . ``` -creates a Docker image than can be used for example with: +which creates a Docker image than can be used for example with: ```bash $ docker run --volume `PWD`:/data/ cerberus:0.1 tests/tcc/00_assignment.c --pp=core ``` diff --git a/backend/cn/README.md b/backend/cn/README.md index d01710fa3..b89883ffe 100644 --- a/backend/cn/README.md +++ b/backend/cn/README.md @@ -18,7 +18,7 @@ and their dependencies. Note: there is a [known bug with Z3 version 4.8.13](https://github.com/rems-project/cerberus/issues/663) (the default on Ubuntu 22.04) so you may wish to install Z3 via opam later for a more - up-to-date version. CVC5 + up-to-date version. Z3 that is provided in the docker images is sufficiently up-to-date. 2. Install the opam package manager for OCaml: https://ocaml.org/docs/installing-ocaml#install-opam.