Stream: Coq Platform devs & users

Topic: Expected installation time of Coq Platform


view this post on Zulip Huỳnh Trần Khanh (Aug 10 2022 at 13:54):

I'm installing the Coq Platform from source. How much time does it take? I'm on a machine with 8 GB of RAM and 4 CPU cores.

view this post on Zulip Karl Palmskog (Aug 10 2022 at 13:56):

the longest-running installations are: CompCert, VST, UniMath. If you avoid those, I think it generally takes less than an hour

view this post on Zulip Notification Bot (Aug 10 2022 at 13:57):

This topic was moved here from #Coq users > Expected installation time of Coq Platform by Karl Palmskog.

view this post on Zulip Huỳnh Trần Khanh (Aug 10 2022 at 16:58):

Hey I got a ton of "The compilation of ... failed at" messages. Is this normal? How should I deal with this?

view this post on Zulip Huỳnh Trần Khanh (Aug 10 2022 at 16:59):

Also the compilation takes very long, even though I didn't choose to install VST and CompCert stuff.

view this post on Zulip Huỳnh Trần Khanh (Aug 10 2022 at 17:01):

I think I need to change course. Maybe it's a much wiser idea to just install base right? And then I can install other stuff later through opam.

view this post on Zulip Huỳnh Trần Khanh (Aug 10 2022 at 18:04):

Nevermind. I interrupted the Coq Platform script midway, then installed QuickChick manually. Things seem to work.

view this post on Zulip Huỳnh Trần Khanh (Aug 10 2022 at 18:11):

Such an exhausting night.

view this post on Zulip Michael Soegtrop (Aug 10 2022 at 18:20):

@Huỳnh Trần Khanh : 8GB is quite tight - you might have to reduce the number of parallel threads from the recommendation. How much did you give?
Usually the "compilation failed" issues are out of memory issues.
You should set the parallelism such that your machine does not swap much. If you set it too high, the compilation needs to much memory and will swap heavily.

view this post on Zulip Michael Soegtrop (Aug 10 2022 at 18:22):

Also it might make sense to not compile VST und UniMath. For VST the script asks, UniMath you can comment out in the package pick file you chose. I should add a question for "packages which take a long time".

view this post on Zulip Karl Palmskog (Aug 10 2022 at 18:22):

usually 4 cores in a machine will result in opam setting 8 jobs per package installation. But then package installations can run in parallel, so I can easily see that 8 GB runs out and swaps until OOM killer kicks in and removes the process

view this post on Zulip Michael Soegtrop (Aug 10 2022 at 18:23):

If you compile everything on a slowish machine with 8GB it can take 4 hours. If you overdo parallelism and your machine swaps, it can take a day.

view this post on Zulip Michael Soegtrop (Aug 10 2022 at 18:23):

@Karl Palmskog : the script asks for the job count and gives some recommendations depending on memory.

view this post on Zulip Michael Soegtrop (Aug 10 2022 at 18:24):

See (https://github.com/coq/platform/blob/main/shell_scripts/ask_parallel_build.sh)

view this post on Zulip Michael Soegtrop (Aug 10 2022 at 18:24):

Possibly the recommendations are outdated - it might also depend on the OS.

view this post on Zulip Karl Palmskog (Aug 10 2022 at 18:25):

OK, I've had trouble with some heavy Coq package installations (not necessarily in the Platform) even with 16 GB memory. Currently, it seems like 32 GB is the sweet spot where one doesn't have to care much. But I hear that for example HOL4+CakeML bootstrapping needs 64+GB these days.

view this post on Zulip Michael Soegtrop (Aug 10 2022 at 18:30):

@Huỳnh Trần Khanh : please post your parallism parameter, OS and memory load here. If 4 threads does not work at 8 GB, I need to adjust the docs.

view this post on Zulip Huỳnh Trần Khanh (Aug 11 2022 at 00:58):

Debian, 8 parallel jobs. When I run htop I see that my RAM is fully used and my machine has to swap to disk.

view this post on Zulip Paolo Giarrusso (Aug 11 2022 at 07:13):

"8 parallel jobs" means up to 64 Coq processes (8 opam packages, each running up to 8 Coq processes); I recall the Platform explains this opam limitation.

view this post on Zulip Paolo Giarrusso (Aug 11 2022 at 07:18):

And even outside the platform, for normal builds where 8 parallel jobs really means 8 (because you just call make or dune, not opam on top) you risk running out of RAM, since a Coq binary can easily take 2GB. A build that swaps to a good SSD probably still have a significant slowdown (haven't tested); if the build swaps to a bad SSD or an actual disk... it's better to stop.

view this post on Zulip Michael Soegtrop (Aug 11 2022 at 07:36):

@Huỳnh Trần Khanh : the script recommends for 8GB the following (at the page where it asks you to enter the number of parallel jobs):

With 8 GB of RAM a sequential package build with 4 make jobs is recommended.

so 4 make jobs and package sequential. This means there are at most 4 Coq jobs but it also means it will take something like 6..8 hours (with VST).
I am not sure if you chose sequential or parallel build. With 8 jobs and parallel build you can end up with 8x8 parallel Coq jobs (well this does not really happen but it can easily be 20), which would be 16x the recommendation. But even if you did run it sequentially, 8 jobs is still too much.

view this post on Zulip Michael Soegtrop (Aug 11 2022 at 07:37):

I expect that if you stick to the recommendation, the build runs through fine and without swapping.

view this post on Zulip Michael Soegtrop (Aug 11 2022 at 07:38):

In case it doesn't work please report an issue giving details of your environment and chosen settings, so that I can experiment and possibly adjust the recommendations.

view this post on Zulip Michael Soegtrop (Aug 11 2022 at 07:54):

Btw.: should I automate these decisions? It is a bit tricky to get the memory size in a system independent way but doable. Again it might make sense to have an advanced mode, which goes into more detail.

view this post on Zulip Michael Soegtrop (Aug 11 2022 at 07:57):

@Huỳnh Trần Khanh : one more note: on CI we run with 2 make jobs and parallel which takes about 6 hours including VST. It might be worthwhile to check if 4+sequential or 2+parallel, which both result in max 4 make jobs, is faster.

view this post on Zulip Théo Zimmermann (Aug 11 2022 at 12:19):

Michael Soegtrop said:

Btw.: should I automate these decisions? It is a bit tricky to get the memory size in a system independent way but doable. Again it might make sense to have an advanced mode, which goes into more detail.

Yes, I think it would be very useful if these decisions could be automated (at least for a large share of users). I think it would be also really nice if the script could print an estimated time with / without long-build packages, based on system configuration, and then ask the user what they want to install.


Last updated: Jan 30 2023 at 12:03 UTC