coq-program-verification-template icon indicating copy to clipboard operation
coq-program-verification-template copied to clipboard

Published 20 hours ago • verified publisher icon coq-community

Cache compcert

Open yforster opened this issue 4 years ago • 2 comments

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?

yforster avatar Oct 13 '20 20:10 yforster

@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 https://github.com/coq-community/docker-coq/issues/12.

palmskog avatar Oct 13 '20 20:10 palmskog

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.

yforster avatar Oct 14 '20 07:10 yforster