bump to nightly-2023-07-25

Stream: batteries

[Kim Morrison]

@Mario Carneiro, would you be able to have a quick look at https://github.com/leanprover/std4/pull/202, and see how you feel about having to split out these rws into separate statements. It feels like a bad regression to me, and that we should ask for https://github.com/leanprover/lean4/pull/2317 to be reverted.

[François G. Dorais]

It is an annoying regression! There's a lot of code I'll need to patch! Perhaps it can be revised so that prior elaborations saved and tried before attempting to elaborate again.

[Kim Morrison]

Pinging @Alex J. Best, too.

[Kim Morrison]

I propose making a revert PR, and then trying again with a solution that either tries to reuse elaborations first, or only has this behaviour on at *.

[Mario Carneiro]

I agree. An alternative implementation strategy for lean4#2317 is to reassign the metavariables created during elaboration of the term

[Kim Morrison]

lean4#2366 is the revert PR.

[Alex J. Best]

My mistake, sorry. I should have tested mathlib more with this change. I just didn't forsee that breakage was even possible.

[Alex J. Best]

Though Mario's suggestion might be quite easy to implement? Unfortunately I'm at a conference today so can't really look into this myself.