reduce l4v/Isabelle image size

seL4 / seL4-CAmkES-L4v-dockerfiles

Dockerfiles defining the dependencies required to build seL4, CAmkES, and L4v.

12 stars 39 forks source link

reduce l4v/Isabelle image size #67

Closed lsf37 closed 7 months ago

lsf37 commented 7 months ago

The l4v image has gotten too large to even just pull from within a GitHub action (about 3GB).

This PR removes some old obsolete settings and reduces the images size:

use default polyml32_64 builds, which go up to 16GB of heap size, which was the max before anyway. This should reduce heap size.
remove vscodium component from cache (saves > 1GB)
remove separate MLTon download, which is now an Isabelle component anyway

lsf37 commented 7 months ago

It looks like l4v is also downloading another ghc installation in addition to what the camkes image already provides. Ideally we should also eliminate that, but if this build succeeds it's already better than before and we should probably make that a separate PR.

lsf37 commented 7 months ago

Btw, the total image size of the l4v image is still about 16GB after this change (down from around 18GB). Probably worth looking into again in the future.

LukeMondy commented 7 months ago

I have a vague memory that the latex packages took up a lot of room. Maybe an l4v-slim image could be made for builds?

lsf37 commented 7 months ago

I have a vague memory that the latex packages took up a lot of room. Maybe an l4v-slim image could be made for builds?

It's possible that this is one of the major contributors, yes. Unfortunately, even some of the basic builds already do need latex (and with a lot of packages), so I don't think we can leave it out.

Two other major blocks of storage are the Isabelle heap images (the cache) and the Isabelle contrib files. I don't think there is much we can do about the heap images, but we could look into removing binaries for other architectures from the contrib install.