perf: worst case n log n complexity for Array.qsort

[johanphenkel-cmd]

This PR optimizes Array.qsort to no longer take quadratic time in the worst case.

Fixes #8087

[TwoFX]

!radar

[leanprover-radar]

Benchmark results for dadc40e against f0ef737 are in. There are significant results. @TwoFX @johanphenkel-cmd @normalifelias

• 🟥 build//instructions: +41.1G (+0.36%)

Large changes (3🟥)

• 🟥 compiled/io_compute//instructions: +4.4G (+38.87%)
• 🟥 misc/leanchecker --fresh Init//instructions: +11.5G (+3.19%)
• 🟥 size/Init/.olean.private//bytes: +5MiB (+2.02%)

Medium changes (1✅, 2🟥)

• 🟥 elab/big_omega//instructions: +185.3M (+0.87%)
• 🟥 elab/big_omega_MT//instructions: +184.9M (+0.86%)
• ✅ elab/bv_decide_large_aig//instructions: -1.0G (-2.55%)

Small changes (75✅, 15🟥)

Too many entries to display here. View the full report on radar instead.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f0ef7372e65860908c8020e146d18acfb8a65248 --onto 659e8bb858995b0a1ada239c5b3819c8f8f2772f. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-12 14:57:04)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase f0ef7372e65860908c8020e146d18acfb8a65248 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-06-12 14:57:05)

[hargoniX]

To catch up you need to at least @[inline] the 4 last wrapper functions, otherwise specialization won't pull the lt argument through all the way.

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 0f291d8 against f0ef737 are in. There are significant results. @hargoniX @normalifelias

• 🟥 build//instructions: +59.9G (+0.53%)

Large changes (6🟥)

• 🟥 compiled/io_compute//instructions: +4.4G (+38.86%)
• 🟥 misc/leanchecker --fresh Init//instructions: +11.3G (+3.15%)
• 🟥 size/Init/.olean.private//bytes: +5MiB (+1.99%)
• 🟥 size/all/.olean.private//bytes: +11MiB (+0.85%)
• 🟥 size/compile/.out//bytes: +15MiB (+0.63%)
• 🟥 size/libleanshared.so//bytes: +1MiB (+0.97%)

Medium changes (1✅, 5🟥)

• 🟥 elab/big_omega//instructions: +243.0M (+1.14%)
• 🟥 elab/big_omega_MT//instructions: +236.4M (+1.10%)
• ✅ elab/bv_decide_large_aig//instructions: -996.2M (-2.48%)
• 🟥 size/all/.c//lines: +66.1k (+0.56%)
• 🟥 size/all/.ir//bytes: +2MiB (+0.60%)
• 🟥 size/install//bytes: +17MiB (+0.57%)

Small changes (1✅, 126🟥)

Too many entries to display here. View the full report on radar instead.

[hargoniX]

That is quite the suprising outcome 🙃