PR !4#31587: Lean pr testing 11156

Stream: triage

[Random Issue Bot]

Today I chose PR #31587 for discussion!

Lean pr testing 11156
Created by @Jovan Gerbscheid (@JovanGerb) on 2025-11-13
Labels: WIP, merge-conflict

Is this PR still relevant? Any recent updates? Anyone making progress?

[Jovan Gerbscheid]

Relevant in the sense that it shows there is a clear performance improvement available. But this would require more investigation to see exactly where the performace improvement comes from. I'm not currently working on this

[Michael Rothgang]

Would lean#11447 be a useful intermediate step? That PR seems to have an approving partial review (though I see no mathlib benchmark).

[Jovan Gerbscheid]

I think I did benchmark it, but it turned out to have no significant impact

[Jovan Gerbscheid]

I think a useful next step would be to split up the changes in this PR and benchmark them separately to see what exactly gives the speedup. But that seems like an annoying amount of work.

[Johan Commelin]

@Jovan Gerbscheid Should this be a PR into master? Or rather into nightly-testing?

[Johan Commelin]

I recently learned about jj (jujutsu) which can be used on git repos, and might make it easier to split this into pieces and stack them on top of each other.

[Johan Commelin]

I've been using it for a few days, but only for trivial things so far.

[Jovan Gerbscheid]

It was only a PR to master in order to do benchmarking. But we now have the new !bench mathlib command which will take care of this automatically.