Cache compcert

[yforster]

It seems like most of the CI time is spent on building the dependencies. Is there a way to tell the CI to cache the files for e.g. CompCert in this GitHub workflow setup, or would this require a docker image with CompCert precompiled?

[palmskog]

@yforster yes, most of the CI time is spent building dependencies (VST, actually). The best way to handle this would likely be to build a dedicated Docker image based on Docker-Coq with the CompCert and VST dependencies included from the start. Erik Martin-Dorel has already done a lot of the automation groundwork for this with his Docker-Base and Docker-Coq Docker files, and in particular with the Docker Keeper tool. See also the discussion in rocq-community/docker-coq#12.

[yforster]

Thanks, that's very helpful!

I'm mainly asking because we have very similar problems in the compilation chain MetaCoq -> coq-library-undecidability -> coq-library-complexity.

I'll have a look whether we can get automation working to create docker images for the first two, or at least create docker images corresponding to opam releases.