speedcenter output

Stream: general

[Kevin Buzzard]

riou.png

Adding Joel Riou as a maintainer has sped up typeclass inference by 15.2% . The PR edits README.md and does nothing more.

[Kevin Buzzard]

The commit does appear to be being compared against the previous commit to master (scroll to bottom in the link below):

http://speedcenter.informatik.kit.edu/mathlib4/compare/452378de-068d-46b9-86cf-41bd58fc402a/to/c8833d5e-4141-4864-ad5a-9483c9fdd6bb

Wall clock compilation time went down by about 20 minutes. Is it just that the machine doing all the work is super-noisy?

[Sebastian Ullrich]

See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/slowness.20in.20ring.20theory.20file/near/380587469

[Matthew Ballard]

Other than these hiccups I’ve found it’s results to be very much reproducible