perf: issue at `binop%` and `binrel%` elaborators

leodemoura commented 1 week ago

This issue was affecting several Mathlib files.

@mattrobball Found where the [nonassignable]s were coming from. Thanks for helping to diagnose this performance issue.

leanprover-community-mathlib4-bot commented 1 week ago

Mathlib CI status (docs):

❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 03040618b8f9b35b7b757858483e57340900cdc4 --onto b1bedbe0d2ba1dd3c654154897013e0399f5a53c. (2024-05-07 02:41:39)
💥 Mathlib branch lean-pr-testing-4085 build failed against this PR. (2024-05-07 04:27:47) View Log
💥 Mathlib branch lean-pr-testing-4085 build failed against this PR. (2024-05-07 05:12:55) View Log
🟡 Mathlib branch lean-pr-testing-4085 build against this PR was cancelled. (2024-05-07 05:25:45) View Log
🟡 Mathlib branch lean-pr-testing-4085 build this PR didn't complete normally. (2024-05-07 05:26:25) View Log
✅ Mathlib branch lean-pr-testing-4085 has successfully built against this PR. (2024-05-07 06:15:00) View Log
✅ Mathlib branch lean-pr-testing-4085 has successfully built against this PR. (2024-05-07 07:22:31) View Log

mattrobball commented 1 week ago

At leanprover-community/mathlib4#12718, I benchmarked a working mathlib with a v4.8.0-rc1 with this commit cherry picked on top.

Overall there is a -400B in instructions driven mainly by one file which was -800B. The issue there was the new CoeT synthesis attempts in Lean.Elab.Term.Op.hasCoe.

semorrison commented 1 week ago

The new slow-downs are pretty severe in Mathlib.AlgebraicGeometry.Restrict.

semorrison commented 1 week ago

I got different speed center results from https://github.com/leanprover-community/mathlib4/pull/12719 than @mattrobball got from https://github.com/leanprover-community/mathlib4/pull/12718; mine are worse, with an overall +500B instructions... The difference probably comes down to exactly where they converge with the master line in Mathlib; we're comparing against different base commits.

mattrobball commented 1 week ago

It's universes triggering the expensive CoeT's.

semorrison commented 1 week ago

Closing in favour of #4092.

leanprover / lean4

perf: issue at `binop%` and `binrel%` elaborators #4085