fix: abstractNestedProofs should see into the head of an application
#7353
Conversation
|
Mathlib CI status (docs):
|
|
Can you fix the tests (again)? |
|
Hmm, this test is really annoying because it keeps changing the order of its messages (hence the merge conflict) |
Head branch was pushed to by a user without write access
|
Actually, given that this is a performance critical function, could you maybe make another measurement with the old code that looks at a full application as a whole (but of course fixed to also visit the function). Partial applications are never proofs, and it may make a difference to not look up the cache for every partial application in the term. (Or maybe the proposed code is better if partial applications are shared - who knows) |
44b063f to
a2bc005
Compare
|
That's a very good point. My suspicion is now that this visiting the partial applications is part of the reason for the slowdown. |
|
Indeed, the benchmark shows that now the slowdown in processing pre-definitions has disappeared. |
|
Great, thanks! |
|
Ah, one last thing: Please update the PR description to reflect this |
This PR changes
abstractNestedProofsso that it also visits the subterms in the head of an application.This oversight caused some definitions in mathlib to have unabstracted proofs, such as CategoryTheory.StructuredArrow.commaMapEquivalenceInverse
Mathlib bench:
build instructions -0,166 %
lint instructions -0.72 %
This speedup comes from files containing
CategoryTheory.Functor, which contains beta unreduced expressions, where abstracting proofs used to not happen.Zulip: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/dsimp.20simplifies.20proofs.2C.20which.20is.20slow/near/503630173