Build a truly multi platform docker image #660

podhrmic · 2024-10-25T19:54:40Z

Fixes #659
Follows the instructions from https://depot.dev/blog/multi-platform-docker-images-in-github-actions

dc-mak · 2024-11-04T14:39:15Z

Dockerfile.deps

+RUN opam switch create with_coq $COMPILER_VERSION && \
+  eval `opam env --switch=with_coq` && \
+  opam repo add --yes --this-switch coq-released https://coq.inria.fr/opam/released && \
+  opam pin --yes -n coq-struct-tact https://github.com/uwplse/StructTact.git && \
+  opam repo add --yes --this-switch iris-dev https://gitlab.mpi-sws.org/iris/opam.git && \
+  opam pin --yes -n coq-sail-stdpp https://github.com/rems-project/coq-sail.git#f319aad && \
+  opam pin --yes -n coq-cheri-capabilities https://github.com/rems-project/coq-cheri-capabilities.git


This is unnecessary, very slow and should be deleted.

dc-mak · 2024-11-04T14:41:46Z

Dockerfile.deps

 RUN apt-get update
 RUN apt-get upgrade -y
-RUN apt-get install -y opam libgmp-dev libmpfr-dev
+RUN apt-get install -y build-essential libgmp-dev z3 opam cmake pkg-config python3-distutils


I believe pkg-config is required for zarith, and build-essential comes via opam, but the rest I'm not sure about?
Also, there's a known-bug with the default Z3 version in Ubuntu 22.04 so maybe a more recent binary release, or installing via opam, is more sensible (opam has version 4.13.0-3).

dc-mak

What's the intended use case for this Dockerfile?

dc-mak · 2024-11-04T14:45:17Z

Dockerfile.deps

+# Install Cerberus
+RUN opam switch $COMPILER_VERSION && \
+  eval `opam env --switch=$COMPILER_VERSION` && \
+  opam pin --yes --no-action add cerberus-lib . && \
+  opam pin --yes --no-action add cerberus . && \
+  opam install --yes cerberus
+
+# Run Cerberus CI tests
+RUN opam switch $COMPILER_VERSION && \
+  eval `opam env --switch=$COMPILER_VERSION` && \
+  cd tests; USE_OPAM='' ./run-ci.sh


These are also unnecessary, you should be able to skip straight to the CN section - it will pick up the dependencies automatically.

dc-mak · 2024-11-04T14:46:29Z

Dockerfile.deps

+RUN opam switch $COMPILER_VERSION && \
+  eval `opam env --switch=$COMPILER_VERSION` && \
+  opam pin --yes --no-action add cn . && \
+  opam install --yes cn ocamlformat.0.26.2


Is the Dockerfile being used for development or as an application? You won't need ocamlformat as an application, but you will for development (and the later source code formatting).

opam install -y ./cerberus.opam /cerberus-lib ./cn.opam should also work without pinning first.

dc-mak · 2024-11-04T14:46:36Z

Dockerfile.deps

+# Check CN code formatting
+RUN opam switch $COMPILER_VERSION && \
+  eval `opam env --switch=$COMPILER_VERSION` && \
+  USE_OPAM='' cd backend/cn && dune build @fmt
+
+# Run CN CI tests


Ditto here.

podhrmic · 2024-11-04T18:26:00Z

What's the intended use case for this Dockerfile?

To run CN on OpenSUT code in a CI: https://github.com/GaloisInc/VERSE-OpenSUT (an example job is here). And more broadly to enable easy CN distribution, such that you don't need to install opam and build everything from scratch.

I think I can make the resulting image much smaller (just the compiled CN binary + basic OS dependencies should be sufficient).

…ith docker build actions

dc-mak · 2024-11-06T11:12:22Z

Ok in that case, it's more as an application than as dev environment. Simply doing opam install -y ./cerberus.opam ./cerberus-lib.opam ./cn.opam should suffice after system deps, opam and correct ocaml version have been installed.

That by itself should be fairly minimal. I don't think CN is linked statically, and so it will need its library dependencies.

podhrmic · 2024-11-06T14:17:45Z

Correct, it is more an application in our use case. Do you think the steps outlined here would work for creating a statically linked binary? I am trying to avoid needing opam/ocaml for various reasons (see GaloisInc/VERSE-Toolchain#48)

dc-mak · 2024-11-06T14:28:52Z

It might work, but we have no experience with trying that and will be unable to help in case it doesn't. I don't see an explicit rejection of the OCaml platform on the link you sent, and opam is availabe on RHEL. But obviously you can proceed as you need to; we can only support with build instructions as given.

podhrmic · 2024-11-06T22:57:46Z

I tried running opam install -y ./cerberus.opam ./cerberus-lib.opam ./cn.opam but it resulted in larger images that when using the Makefile steps.

I also added a RedHat image to the build.

This reverts commit 5afd280.

podhrmic · 2024-11-07T01:07:06Z

@dc-mak I believe the MR is now ready. The docker build works, but the image is not being pushed into the registry - I think this will be resolved for master builds. I also added more CI badges to the README.

dc-mak · 2024-11-07T11:09:42Z

Dockerfile.redhat

+RUN opam install --deps-only  ./cerberus-lib.opam ./cn.opam
+
+RUN eval `opam env` \
+  && make install \


This line is not necessary.

dc-mak · 2024-11-07T11:10:22Z

Dockerfile.redhat

+
+ENV OPAMCONFIRMLEVEL=unsafe-yes
+RUN opam init --disable-sandboxing
+RUN opam install dune lem


This line is unnecessary too.

@dc-mak

* Simplify the docker build, and properly build a multiplatform image with docker build actions * Temporarily disable scheduled docker build for faster testing * Clean up the release docker image * Add a separate job for RedHat docker image * Added RedHat dockerfile * Revert "Temporarily disable scheduled docker build for faster testing" This reverts commit 5afd280. * Try to specify github tokens * Add CI badges: * Remove un-needed lines per @dc-mak 's suggestions

podhrmic marked this pull request as ready for review October 25, 2024 19:54

This was referenced Oct 28, 2024

Build multiplatform docker image #656

Closed

Update CN version GaloisInc/VERSE-OpenSUT#127

Merged

podhrmic mentioned this pull request Oct 29, 2024

Trusted Boot: firmware.c has passing specs for all functions GaloisInc/VERSE-OpenSUT#123

Merged

7 tasks

dc-mak reviewed Nov 4, 2024

View reviewed changes

Simplify the docker build, and properly build a multiplatform image w…

3d9a7b6

…ith docker build actions

podhrmic force-pushed the 659-docker-image-manifest branch from 3450832 to 3d9a7b6 Compare November 6, 2024 19:41

podhrmic added 4 commits November 6, 2024 11:43

Temporarily disable scheduled docker build for faster testing

5afd280

Clean up the release docker image

31f2e19

Add a separate job for RedHat docker image

45da802

Added RedHat dockerfile

3f67691

podhrmic mentioned this pull request Nov 6, 2024

Ubi9 based Dockerfile #650

Closed

podhrmic added 3 commits November 6, 2024 16:41

Revert "Temporarily disable scheduled docker build for faster testing"

7bf0f99

This reverts commit 5afd280.

Try to specify github tokens

12c844f

Add CI badges:

72a5c6e

dc-mak reviewed Nov 7, 2024

View reviewed changes

Remove un-needed lines per @dc-mak 's suggestions

a584f50

dc-mak merged commit e4de4e4 into rems-project:master Nov 7, 2024
4 checks passed

podhrmic deleted the 659-docker-image-manifest branch November 7, 2024 16:41

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Build a truly multi platform docker image #660

Build a truly multi platform docker image #660

podhrmic commented Oct 25, 2024 •

edited

Loading

dc-mak Nov 4, 2024 •

edited

Loading

dc-mak Nov 4, 2024 •

edited

Loading

dc-mak left a comment

dc-mak Nov 4, 2024

dc-mak Nov 4, 2024

dc-mak Nov 4, 2024 •

edited

Loading

dc-mak Nov 4, 2024

podhrmic commented Nov 4, 2024

dc-mak commented Nov 6, 2024 •

edited

Loading

podhrmic commented Nov 6, 2024

dc-mak commented Nov 6, 2024

podhrmic commented Nov 6, 2024

podhrmic commented Nov 7, 2024

dc-mak Nov 7, 2024

dc-mak Nov 7, 2024

Build a truly multi platform docker image #660

Build a truly multi platform docker image #660

Conversation

podhrmic commented Oct 25, 2024 • edited Loading

dc-mak Nov 4, 2024 • edited Loading

Choose a reason for hiding this comment

dc-mak Nov 4, 2024 • edited Loading

Choose a reason for hiding this comment

dc-mak left a comment

Choose a reason for hiding this comment

dc-mak Nov 4, 2024

Choose a reason for hiding this comment

dc-mak Nov 4, 2024

Choose a reason for hiding this comment

dc-mak Nov 4, 2024 • edited Loading

Choose a reason for hiding this comment

dc-mak Nov 4, 2024

Choose a reason for hiding this comment

podhrmic commented Nov 4, 2024

dc-mak commented Nov 6, 2024 • edited Loading

podhrmic commented Nov 6, 2024

dc-mak commented Nov 6, 2024

podhrmic commented Nov 6, 2024

podhrmic commented Nov 7, 2024

dc-mak Nov 7, 2024

Choose a reason for hiding this comment

dc-mak Nov 7, 2024

Choose a reason for hiding this comment

podhrmic commented Oct 25, 2024 •

edited

Loading

dc-mak Nov 4, 2024 •

edited

Loading

dc-mak Nov 4, 2024 •

edited

Loading

dc-mak Nov 4, 2024 •

edited

Loading

dc-mak commented Nov 6, 2024 •

edited

Loading