performance of ordered refactor

Stream: general

[Damiano Testa]

There has been a discussion about performance issues with the refactor #7574 .

I'm all in favour for checking this, but I have no idea where to start. Also, given the option, I would like to test out the alternative approach that I had in mind, which would only introduce 2 typeclasses instead of 16, but each one taking two functions as inputs.

Where can I start to learn about checking these things? Would simply pushing to the github and monitoring the time CI takes to build the PRs be a good measure? Would comparing the local build times on my machine be better? I am really completely a novice in this, so any commentary, however silly it might appear, could be an eye-opener for me!

Thanks!

[Eric Wieser]

set_option profiler true can help you time specific proofs

[Damiano Testa]

Ok, but I get somewhat inconsistent timings when I use it: recompiling the same lemma does not always give the same time. I have an impression that we are talking about a small discrepancy on average, which might be difficult to spot on a single lemma. Maybe I am wrong though...

[Sebastien Gouezel]

I think compiling the whole library is the only relevant measure here, since it is the addition of a lot of small stuffs. How to get reliable timings when compiling the whole library is outside of my competence domain, though (one-threaded? No heavy task running at the same time?)

[Eric Rodriguez]

it may be worth at some point branching the library 5 times or something, and running a full CI suite on it to see what the variance on times are
(obviously at a quiet CI time)

[Damiano Testa]

Ok, thanks for the suggestions! Right now, I am waiting for the first successful build of the first branch. On my machine it built with no errors, so I am hopeful!

[Damiano Testa]

Later this week, I hope to prepare the "competitor" PR and see how they compare, so there is plenty of time for further suggestions and how to implement them! :smile:

[Anne Baanen]

@Jannis Limperg has (used to have?) a build server that can do these kinds of timings.

[Jannis Limperg]

I can make a timing of this branch on the hardware (or rather VM) used for the benchmark bot. It's not amazingly precise, but it'll spot bigger performance regressions. Just give me the relevant commit.

[Damiano Testa]

Jannis, that would be great! If you could time commit

df080022c2ba78f1969f15da0975295fd5e384f7

I would be very grateful! I will be preparing a second PR to compare it with this one, but for the moment, simply seeing how this one compares with the current master would be awesome!

Thanks a lot! And let me know if you need anything else!

[Damiano Testa]

For definiteness, I would like to compare these two commits:

• current-ish master
  a7e1696f5b1bd29f1575d99162e9f80141b28e4c

• first working refactor in adomani_new_order_typeclasses_2
  df080022c2ba78f1969f15da0975295fd5e384f7

[Damiano Testa]

Once I have a working alternative refactor, I will post the commit hash as well, so that the three can be compared for relative performance.

@Jannis Limperg , let me know if this is asking too much, of course! I realize that it is not fun to have a computer building stuff just to see what is faster/slower!

[Damiano Testa]

Actually, @Jannis Limperg , if you have not started the timings, it might be better to hold off a little bit. I just realized that the version of master that I proposed was one where Mario made a change to avoid some timeouts, whereas the version of the commit that I wanted to compare does not have those changes!

So, I am now building two branches with the two proposed refactors, but with the current master. Once I am sure that they pass all the tests, I will give the commit hashes for these branches so that the three versions can be timed!

Again, thanks a lot for your help!

[Jannis Limperg]

No worries! All I need to do is log on to the server and type one command, so it's no big deal. Please ping again when you have the relevant commits.

[Damiano Testa]

Ok, thanks @Jannis Limperg !

Here are the three commits that I would like to test for relative speed (they just finished building):

• the version of master out of which the two commits below branched
  a7e1696f5b1bd29f1575d99162e9f80141b28e4c

• the refactor in adomani_new_order_typeclasses_2, with 16 new typeclasses
  88d6a72d98b13d5bcae1a4560260cae17f60d309

• the refactor in adomani_ordered_stuff, with 2 new typeclasses
  03b502c386905abef9892d59d09c36220c04a0da

Unless I messed up, I merged the commit of master above into the two branches below, fixed what needed fixing and then I would like to time the three commits. This should hopefully minimize time unrelated to the specific changes that I am interested in, since they all contain the "same" copy of master.

[Jannis Limperg]

:+1: The builds are running now. They'll probably take until tomorrow since I'm doing single-threaded builds on weak hardware.

[Damiano Testa]

That's great, thank you very much!

I do not mind if they take long, I am in no rush and I prefer to get more reliable relative timing than "smartest and quickest possible build time"!

[Yaël Dillies]

If it takes longer, then the precision might actually be increased!

[Damiano Testa]

@Jannis Limperg , while I am not in a rush, I am curious to know the outcome of the timing: any results yet? :smile:

[Jannis Limperg]

• a7e1696f5b1bd29f1575d99162e9f80141b28e4c: 2h15m49s/2h16m15s
• 88d6a72d98b13d5bcae1a4560260cae17f60d309: 2h17m16s/2h16m3s
• 03b502c386905abef9892d59d09c36220c04a0da: 2h12m28s

I did two runs per commit but the second run for the last commit failed for some strange reason (not related to the code). But I think the picture is clear enough anyway. The build time typically fluctuates +/- 1min, so the difference between the first two commits is probably not significant.

[Damiano Testa]

Ok, great, thank you very much for this!!