Huỳnh Trần Khanh (Aug 10 2022 at 13:54): 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.
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
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.
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?
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.
Huỳnh Trần Khanh (Aug 10 2022 at 17:01):How could I self diagnose this? I would like to see the build output of the failed make commands.
The packages that I couldn't install are coq-flocq3, coq-flocq, coq-stdpp, coq-hierarchy-builder, coq-mathcomp-ssreflect and coq-coqprime.
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.
Huỳnh Trần Khanh (Aug 10 2022 at 18:11):Such an exhausting night.
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.
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".
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
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.
Michael Soegtrop (Aug 10 2022 at 18:23):@Karl Palmskog : the script asks for the job count and gives some recommendations depending on memory.
Michael Soegtrop (Aug 10 2022 at 18:24):See (https://github.com/coq/platform/blob/main/shell_scripts/ask_parallel_build.sh)
Michael Soegtrop (Aug 10 2022 at 18:24):Possibly the recommendations are outdated - it might also depend on the OS.
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.
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.
Huỳnh Trần Khanh (Aug 11 2022 at 00:58):Debian, 8 parallel jobs. opam packages built in parallel. When I run htop I see that my RAM is fully used and my machine has to swap to disk. Usually my rule of thumb is running 8 parallel jobs works fine on my machine. Seems like this works for C/C++ and Rust but not for Coq.
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.
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.
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.
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.
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.
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.
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.
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: Apr 20 2024 at 00:02 UTC