Karl Palmskog (Sep 04 2020 at 11:03): Karl Palmskog (Sep 04 2020 at 11:03):Given that the topic of repo organization was recently raised by Anton in coq-community, I'm thinking of doing a tutorial/template GitHub repo for a Coq program verification project, using platform packages via opam, dune, etc. One fun example would be the line-by-line C version of this program: http://ai.googleblog.com/2006/06/extra-extra-read-all-about-it-nearly.html
Michael Soegtrop (Sep 04 2020 at 12:03):In case you need me to press a bit on pushing opam changes, please let me know.
One note on using opam install with a bunch of packages directly: it can easily lead to out of memory build failures. It actually does require special considerations to build what you would need for this on machines with 4 or 8 GB of RAM. 16 GB is fairly safe and 32 GB is safe on usual PCs. The next Coq platform script takes care of this.
The example is interesting and shows how implicit assumptions change over time. An array of length > 2^30 was not imaginable when this code was written - today with big data it is not that much.
Karl Palmskog (Sep 04 2020 at 12:05):The GitHub Actions CI works well so far, and one can partition lemmas in files to avoid memory use
Michael Soegtrop (Sep 04 2020 at 12:07):Yes, on VMs it is usually easier cause the core count is small. 2 threads at 4GB is usually OK. 4 threads at 4GB needs to mess around with the job limits of opam. You can buy laptops with 16 threads and 4 GB of RAM.
Karl Palmskog (Sep 04 2020 at 12:11):I think the biggest difference would be if we set up Docker images for the 8.12 platform hosted in Docker Hub
Karl Palmskog (Sep 04 2020 at 12:12):basically with a one-line change in the Actions CI config, checking time for anything with VST/Flocq/Coquelicot/MathComp drops from 1 hour to a few minutes
Michael Soegtrop (Sep 04 2020 at 12:44):Indeed - I am almost there with the beta1. The main remaining issue is on Mac, so I could do an alpha4 release and we could start working on a docker image.
Karl Palmskog (Sep 04 2020 at 12:47):@Michael Soegtrop have you thought about how Docker images should be hosted/managed? Do we hook into Érik's existing infrastructure?
Michael Soegtrop (Sep 04 2020 at 12:50):No, I didn't think much about Docker beyond that I think it is desirable in the interest of people's time and the environment and that there are people out there who can help me with it.
Karl Palmskog (Sep 04 2020 at 12:53):it might make sense to make Érik's particular chosen flavor of Debian the "offical Coq Platform on Linux". At least it can serve as the way to validate a full platform installation on Linux.
Michael Soegtrop (Sep 04 2020 at 13:07):Do you have some pointers for me?
Karl Palmskog (Sep 04 2020 at 13:09):https://github.com/coq-community/docker-base https://github.com/coq-community/docker-coq -- it's basically just Debian 10 at the core, but he has done a great job of making everything configurable and integratable with Docker infrastructure
Karl Palmskog (Sep 04 2020 at 13:10):I thought his presentation/slides at the Coq Workhop were very good, but you might have already seen those: https://coq-workshop.gitlab.io/2020/slides/Coq2020_02-02-docker-slides.pdf https://coq-workshop.gitlab.io/2020/abstracts/Coq2020_02-02-docker.pdf
Michael Soegtrop (Sep 04 2020 at 13:13):I wonder how to get forward on this. As a start should I just fork one or the other repo (I guess the second) and make a branch for coq-platform?
Karl Palmskog (Sep 04 2020 at 13:14):I think we should ask for Érik's advice.
Karl Palmskog (Sep 05 2020 at 09:35):I wrote up and posted about the template repo: https://coq.discourse.group/t/a-template-for-organizing-a-coq-program-verification-project/1039
Erik Martin-Dorel (Sep 10 2020 at 17:56):Michael Soegtrop said:
I wonder how to get forward on this. As a start should I just fork one or the other repo (I guess the second) and make a branch for coq-platform?
Hi @Michael Soegtrop, no I don't think creating a fork or a separate branch of the docker-coq github repo is useful;
I'd rather suggest creating a fork of the gitlab repo https://gitlab.com/erikmd/docker-keeper-template in your own gitlab namespace (no need for setting up coqbot), or in https://gitlab.com/coq-community if you prefer, then adapt the Dockerfile and the images.yml
Feel free to ask if you'd like that we arrange some visio/audio meeting, to further discuss the setup of this Docker deployment for coq-platform.
Last updated: Jun 03 2023 at 05:01 UTC