slow builds with Coq 8.19 and/or dune 3.14.0 about coq-hott

[jdchristensen]

Two of the three slowdowns are fixed, so I'll close this. Thanks for your quick fixes, @ejgallego!

[SkySkimmer]

Coq 8.19 is slower than Coq 8.18.

Cost of sort polymorphism.

[jdchristensen]

Cost of sort polymorphism.

@SkySkimmer Thanks for explaining. Is that expected to be in the 5-8% range? Are there plans to improve this?

[Alizter]

Regarding the speed of Dune, I've definitely noticed a regression in the past few versions, but I am not certain the cause of it. I haven't been involved with working on Dune as of late, so I am not certain what the problem is.

Regarding how Dune chooses jobs, this is up to the scheduler of Dune and is not something that is easily tweaked externally AFAIK. There is an option to dump a flame graph of the build detailed here: https://dune.readthedocs.io/en/stable/advanced/profiling-dune.html this should allow you to quickly find bottlenecks and see where the build is spending the most time.

cc @ejgallego for the performance regression in Dune.

[jdchristensen]

I also tested -j1 builds with make 4.3, and Coq 8.19 is 3.2% slower than Coq 8.18. These timings are more stable, so this is probably a more accurate measure of the difference. My -j8 times above with make show 8.19 7.7% slower, but I think one of those 8.18 runs got especially lucky. Further tests show a difference of more like 5%, still more than the -j1 difference.

[ejgallego]

Thanks for the numbers @jdchristensen , they are very useful!

I'll suggest we handle the two performance problems here as different issues, as they really are. Coq performance regression will likely be improved upstream, but indeed, there is an expected slowdown for HoTT. Here HoTT is a bit unlucky I do believe as it is more impacted than other developments.

Regarding the regression in Dune, that's a bit more worrying and deserve investigation.

@jdchristensen , what are the times for the "zero" build on different dune versions?

[by zero build we mean doing dune build when the build is already completed, to measure the overhead of Dune itself re-checking everything has been properly built]

[jdchristensen]

@ejgallego I timed dune build --cache=disabled --display=quiet when nothing needs to be built:

dune 3.14.0:  5.9s
dune 3.11.1:  3.3s
make 4.3:     0.6s

(I added make to the list, but I know that it's not a fair comparison, as dune is doing more sophisticated checks, not just checking timestamps.)

I used those dune flags for the earlier tests as well. --display=quiet is important when timing.

[jdchristensen]

@ejgallego Is it possible to change dune versions in my ocaml switch without having to recompile coq each time? That would make it faster for me to try 3.12 and 3.13, in case that helps. OTOH, you can probably check out the Coq-HoTT library and reproduce these numbers. It has no extra dependencies and builds with "dune build".

[jdchristensen]

@SkySkimmer Another comment is that the HoTT library doesn't use Prop or SProp, so it's a bit unfortunate that the ability to generalize to those slows down the HoTT library. Is there a way to turn off sort polymorphism, or even to completely disable Prop and/or SProp?

[SkySkimmer]

no.

[ejgallego]

@ejgallego Is it possible to change dune versions in my ocaml switch without having to recompile coq each time? That would make it faster for me to try 3.12 and 3.13, in case that helps. OTOH, you can probably check out the Coq-HoTT library and reproduce these numbers. It has no extra dependencies and builds with "dune build".

Yes, it is possible to use any dune regarless of what you have in your opam switch.

Dune itself is self-contained, so it doesn't depend on what is on the switch, except for reading the list of installed packages.

So for example you can compile dune in ~/external/dune/_build/install , the version you want, and then just call that dune instead of the dune in the path.

Important note tho: due to versioning, it is hard to use an older dune with a switch with the newer dune; while dune works, it will complain about install dune packages being newer than what it knows.

So indeed, it is best to work on a switch that has the lowest dune version you plan to test.

[ejgallego]

@jdchristensen , we have identified two performance regressions, indeed there was one from 3.11 to 3.14 and another one long time ago, when we switched dune to a single coqdep call.

Zero build times for me are now under 0.2 seconds, with the following PR applied:

• ocaml/dune#10116

There is another PR that fixes the regression from 3.11 to 3.14, but actually, that regression is not observable after that one is applied.

[ejgallego]

If you are curious about testing, that can be done with:

$ cd dune_git_working_dir
$ hub checkout https://github.com/ocaml/dune/pull/10116
$ make clean && make release
$ DUNE_BIN=$(pwd)/_build/install/default/bin/dune
$ cd hott_working_dir
$ $DUNE_BIN build # etc...

[jdchristensen]

@ejgallego This is wonderful! On my machine, dune now takes 0.16s for a zero build, even faster than make! The -j8 times are also much improved. I've updated the tables:

coq 8.18 / make 4.3:     35.0
coq 8.18 / dune 3.11.1:  36.6
coq 8.18 / dune + PR:    32.3

coq 8.19 / make 4.3:     37.9
coq 8.19 / dune 3.11.1:  38.6
coq 8.19 / dune 3.14.0:  41.9
coq 8.19 / dune + PR:    33.6

Zero build:

dune 3.14.0:  5.9
dune 3.11.1:  3.3
make 4.3:     0.6
dune + PR:    0.16

BTW, my custom build of dune reports its version as 3.12.0-642-gc5fdf4f. I was expecting to see 3.14 or 3.15, not 3.12. Is that expected?

[ejgallego]

@jdchristensen , that's great! Sorry for that bug, these kind of bugs (missing a memoized table) are actually pretty hard to track / test for; there are not so many parts of dune that do this, as usually things are cached in files (for that Dune provides a much better hardened API)

Indeed, when I decided to start working on Coq + Dune, I had made some benchs, and Dune always outperformed make, so I'm glad to see that's still the case in a bug-free setup.

Again thanks for the very important work of performance testing dune and make.

BTW, my custom build of dune reports its version as 3.12.0-642-gc5fdf4f. I was expecting to see 3.14 or 3.15, not 3.12. Is that expected?

I think that dune will use git describe --tags to determine the version, so likely the problem is that the tags are not placed in the main dune branch. If that's the case, that deserves a bug report for Dune, tho I think this may be already be reported.

[jdchristensen]

I think that dune will use git describe --tags to determine the version, so likely the problem is that the tags are not placed in the main dune branch. If that's the case, that deserves a bug report for Dune, tho I think this may be already be reported.

@ejgallego Yes, I can confirm that git log on the main branch shows 3.12.0 as the most recent tag. I couldn't find an issue for this in the dune github issues, but maybe I missed it. Do you want me to open one?

[ejgallego]

Thanks for confirming this, I did open the issue myself, as to provide a bit more info (this is due to a change in Dune's release process)

Here it is ocaml/dune#10141

Thanks again @jdchristensen !

[ejgallego]

IMHO this issue can be closed, dune releases every 6 weeks, so the fix should arrive to the released package pretty soon.

[ejgallego]

Indeed the Coq slowdown won't have an easy fix, but hopefully other improvements in 8.20 will offset this bad case for HoTT.