Is there any reason why the Windows CI is almost 3 times slower than MacOS?
Cygwin is not that fast when it comes to shuffling around 10.000s of files. But I don't see a factor of 3 in Coq Platform CI. I would say it is more between 1.5 and 2 - it is a bit hard to judge, because the package selection is not identical (some plugins simply don't work on Windows). If you see a factor of 3 I would expect that you are so short on memory that there isn't much of a disk cache - which is quite essential for Coq build performance. If this is of interest, I could run local tests with identical package lists and sufficient memory.
My last successful checks here shows 33 minutes for MacOS and 86 for Windows (hosted on Github, IIUC), so the Windows checks are 260% slower than MacOS's for this run. Maybe it was just some random perturbation and the hardware is also probably different.
On Windows in the case you linked about 25 minutes - from 7:02:14 to 7:27:38 -are for installing cygwin. This can take also < 5 minutes - it depends mostly on the download speed of the repos. If you subtract these 25 minutes from the 86, it gets more reasonable.
There would be two ways around this:
Thank you very much for your insight. So it would certainly be worth it to zip cygwin. If that can save 25 minutes for each run it would be huge win.
I can supply such an option to my scripts. Can we host a file with a few GB on github? The unzipping should still take a few minutes.
One can also think about stripping down cygwin - in the last years more and more packages have been added to the default setup. My scripts only add the the default setup, but don't remove packages from it (not sure how one would do this from the command line ...).
Michael Soegtrop said:
I can supply such an option to my scripts. Can we host a file with a few GB on github? The unzipping should still take a few minutes.
I have no idea, but we can try. We still have https://github.com/coq/prerequisites/releases that we can use for this.
I will give it a try.
The setup-ocaml
action has some tricks I believe to cache / sped things up on Windows, maybe worth having a look at what they do too?
Last updated: Oct 13 2024 at 01:02 UTC