Testing slowdown

Stream: mathlib4

[Jeremy Tan]

@Mario Carneiro It's most likely the Std bump that causes the slowdown

Testing on https://github.com/leanprover-community/mathlib4/actions/runs/7574508760 took 1m 14s
Testing on the immediately succeeding bump https://github.com/leanprover-community/mathlib4/actions/runs/7577745057 took 3m 34s

[Mario Carneiro]

I'm suspecting std_exact?

[Mario Carneiro]

https://github.com/leanprover/std4/compare/1d85fd7db28700b28043d6370dd1ebc426de4d5d...1972e073b3e6bc0776ad5b544bfa7db7fc3f7c36

[Mario Carneiro]

the only thing in there which looks like it could affect performance is std#527 (cc: @Scott Morrison )

[Kim Morrison]

Mathlib commits are d8b1dddbc5a6bbaef465befedc9ffdcc35e1a30f (before, fast) and b71c5f26d2d017eac8f6c3403db93603ce7dd95c (after, slow).

[Kim Morrison]

hyperfine reports no essential timing difference in test/LibrarySearch/basic.lean between those commits.

[Kim Morrison]

I'll leave hyperfine running against make test, but for now I'm skeptical? @Jeremy Tan , has this persisted across later CI runs?

[Jeremy Tan]

Scott Morrison said:

has this persisted across later CI runs?

Yes: in the latest staging commit https://github.com/leanprover-community/mathlib4/actions/runs/7635237217/job/20800326296 testing took 4 minutes

[Mario Carneiro]

maybe we should print the results of time lake env lean to the logs

[Kim Morrison]

hyperfine confirms it is real:

kim@carica mathlib4-2 % git checkout b71c5f26d2d017eac8f6c3403db93603ce7dd95c && lake exe cache get && lake build && hyperfine "make test"
Previous HEAD position was d8b1dddbc5 feat(Algebra/Ring/CentroidHom): central iff mul op commute (#8663)
HEAD is now at b71c5f26d2 chore: bump Std to leanprover/std4#541 (#9828)
info: std: updating repository './.lake/packages/std' to revision '1972e073b3e6bc0776ad5b544bfa7db7fc3f7c36'
info: aesop: updating repository './.lake/packages/aesop' to revision '1c638703ed1c0c42aed2687acbeda67cec801454'
No files to download
Decompressing 4143 file(s)
unpacked in 3499 ms
Benchmark 1: make test
  Time (mean ± σ):     296.807 s ±  1.392 s    [User: 258.841 s, System: 59.151 s]
  Range (min … max):   295.400 s … 298.805 s    10 runs

kim@carica mathlib4-2 % git checkout d8b1dddbc5a6bbaef465befedc9ffdcc35e1a30f && lake exe cache get && lake build && hyperfine "make test"
Previous HEAD position was b71c5f26d2 chore: bump Std to leanprover/std4#541 (#9828)
HEAD is now at d8b1dddbc5 feat(Algebra/Ring/CentroidHom): central iff mul op commute (#8663)
info: std: updating repository './.lake/packages/std' to revision '1d85fd7db28700b28043d6370dd1ebc426de4d5d'
info: aesop: updating repository './.lake/packages/aesop' to revision '2ae78a474ddf0a39bc2afb9f9f284d2e64f48a70'
No files to download
Decompressing 4142 file(s)
unpacked in 3524 ms
Benchmark 1: make test
  Time (mean ± σ):     214.860 s ±  4.340 s    [User: 176.060 s, System: 59.337 s]
  Range (min … max):   211.233 s … 222.768 s    10 runs

I'm not going to have a change to look at this until next Monday, if anyone wants to investigate!