search

seL4 / seL4-CAmkES-L4v-dockerfiles

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

l4 docker container is too large #73

Closed lsf37 closed 4 months ago

lsf37 commented 5 months ago

The uncompressed disk size of the l4v docker container is currently 17.8GB -- this is after several attempts at size reduction (was temporarily around 20GB).

For interactive use, this is large, but otherwise perfectly fine. For GitHub use, it is too much, because the disk quota for a GitHub runner is 14GB. That means just pulling and extracting the image will make the job run out of disk space.

We could try to produce a l4v-slim base image that is missing more Isabelle components and doesn't have the Haskell stack cache set up. It could potentially also be missing some other packages, although pretty much all of them are required at some point for l4v to work.

lsf37 commented 5 months ago

The current symptom of this is that the job Deploy C Parser Builder fails, running out of disk space while pulling the image, e.g. https://github.com/seL4/ci-actions/actions/runs/8438055712.

lsf37 commented 4 months ago

Giving up on reducing the size, there is not much that can be removed. Solved the C parser builder issue by basing it on a different image (sel4 instead of l4v).