search

seL4 / seL4-CAmkES-L4v-dockerfiles

Dockerfiles defining the dependencies required to build seL4, CAmkES, and L4v.
12 stars 39 forks source link

Make platform of image explicit #57

Closed Ivan-Velickovic closed 1 year ago

Ivan-Velickovic commented 1 year ago

Specify that the Docker image to be built and run is x86_64 Linux. This is required for non-x86 hosts such as Apple Silicon computers.

Signed-off-by: Ivan Velickovic i.velickovic@unsw.edu.au

axel-h commented 1 year ago

Seem ok to me, does not harm on x86 and appears to help Mac users then. Is this just for building or are you also running x86 containers there via an emulation layer?

Ivan-Velickovic commented 1 year ago

This is what I needed to get the Docker container building & running on an M1 (specifically to run seL4test and other seL4 projects), I'm not using Rosetta. I believe by default if the platform isn't specified Docker will try grab an ARM64 image, which we don't currently support.

lsf37 commented 1 year ago

Fixing the platform to amd64 will mean the image runs under emulation on the M1 (not Rosetta, but whatever docker uses to simulate amd64, I believe it's qemu). For what I've tried so far, this seemed to be working fine and with reasonable performance.

It might also be possible to build a native arm64 image, but that would be a more invasive change (e.g. would need all toolchains etc in arm64 versions). For now I think emulation is fine.

lsf37 commented 1 year ago

@Ivan-Velickovic the build test is now passing. Did you still have issues with Haskell stack in the container?

Ivan-Velickovic commented 1 year ago

@Ivan-Velickovic the build test is now passing. Did you still have issues with Haskell stack in the container?

Yes. For context, trying to invoke stack causes the Linux kernel to kill the process as the system runs out of memory (with 4GiB of memory for the container). Increasing this to 6GiB at least allowed me to successfully do stack --version, however, attempting to build an seL4 project that uses CapDL still failed.

So the main caveat with this PR is that not all seL4 projects will build on M1. I suspect something is going wrong with QEMU's x86_64 -> AArch64 emulation, not sure.

Ivan-Velickovic commented 1 year ago

Superseded by https://github.com/seL4/seL4-CAmkES-L4v-dockerfiles/pull/65.