isDefEq cache for terms not containing metavariables.#2644
Merged
leodemoura merged 7 commits intomasterfrom Oct 14, 2023
Merged
isDefEq cache for terms not containing metavariables.#2644leodemoura merged 7 commits intomasterfrom
leodemoura merged 7 commits intomasterfrom
Conversation
Member
Author
|
!bench |
a0ba45c to
8ba8496
Compare
Member
Author
|
!bench |
Collaborator
|
Here are the benchmark results for commit a0ba45c. Benchmark Metric Change
===================================================
+ lake build clean branch-misses -2.5% (-36.0 σ) |
Collaborator
|
Here are the benchmark results for commit 8ba8496. Benchmark Metric Change
======================================================
+ lake build clean branch-misses -2.5% (-23.8 σ)
+ stdlib tactic execution -7.5% (-23.1 σ) |
ghost
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Oct 10, 2023
|
kim-em
added a commit
to kim-em/std4
that referenced
this pull request
Oct 10, 2023
kim-em
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Oct 10, 2023
kim-em
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Oct 10, 2023
kim-em
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Oct 10, 2023
Collaborator
|
Unfortunately the Mathlib test: is now taking forever! This test was introduced in leanprover-community/mathlib4#5740. |
Member
|
@semorrison Hmm, this at least seems fine on my machine? |
Collaborator
|
Oh, dear! This test has been failing for a while on Apple Silicon (which we don't test in CI). It's not relevant to this PR. |
Member
|
!bench |
Collaborator
|
Here are the benchmark results for commit 5afb7a5. Benchmark Metric Change
======================================================
+ lake build clean branch-misses -2.4% (-23.8 σ)
+ stdlib tactic execution -8.4% (-49.9 σ) |
ghost
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Oct 10, 2023
Collaborator
|
After @Kha's change there are still many regressions in Mathlib: leanprover-community/mathlib4#7606 |
Member
Author
|
!bench |
Collaborator
|
Here are the benchmark results for commit a84dad5. Benchmark Metric Change
======================================================
- lake build clean branch-misses 1.7% (15.9 σ)
- lake env branch-misses 2.8% (10.2 σ)
+ stdlib tactic execution -6.8% (-75.1 σ) |
ghost
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Oct 11, 2023
timotree3
reviewed
Oct 11, 2023
Contributor
timotree3
left a comment
There was a problem hiding this comment.
A couple cleanups to comments
Co-authored-by: Timo <timorcb@gmail.com>
Contributor
|
That looks like a defeq abuse problem to me; |
Contributor
|
[Meta.isDefEq] ❌ FunLike.coe { toFun := ?f } =?= FunLike.coe { toFun := some } ▼
[] ✅ ?α =?= α ▶
[] found messy fun a ↦ (fun x ↦ ?β) a =?= fun a ↦ WithTop α
[] ✅ { toFun := ?f } =?= { toFun := some } ▶
[] ✅ α ↪ Option α =?= α ↪ WithTop α ▶
[] ✅ Function.instFunLikeEmbedding =?= Function.instFunLikeEmbedding ▶
[] ❌ fun a ↦ (fun x ↦ Option α) a =?= fun a ↦ WithTop α ▼
[] ✅ α =?= α
[] ❌ (fun x ↦ Option α) a =?= WithTop α ▼
[] ❌ Option α =?= WithTop α ▼
[] ❌ Option =?= WithTop
[onFailure] ❌ Option α =?= WithTop α
[onFailure] ❌ Option α =?= WithTop α
[onFailure] ❌ FunLike.coe { toFun := ?f } =?= FunLike.coe { toFun := some }
[onFailure] ❌ FunLike.coe { toFun := ?f } =?= FunLike.coe { toFun := some }vs [Meta.isDefEq] ✅ FunLike.coe { toFun := ?f } =?= FunLike.coe { toFun := some } ▼
[] ✅ ?α =?= α ▶
[] found messy fun a ↦ (fun x ↦ ?β) a =?= fun a ↦ WithTop α
[] ✅ { toFun := ?f } =?= { toFun := some } ▶
[] ✅ α ↪ Option α =?= α ↪ WithTop α ▶
[] ✅ Function.instFunLikeEmbedding =?= Function.instFunLikeEmbedding ▶
[] ✅ fun a ↦ (fun x ↦ Option α) a =?= fun a ↦ WithTop α ▼
[] ✅ α =?= α
[] ✅ (fun x ↦ Option α) a =?= WithTop α ▼
[] ✅ Option α =?= WithTop α |
PatrickMassot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Oct 13, 2023
Excluding new rfl and nolint.
kim-em
approved these changes
Oct 13, 2023
Collaborator
kim-em
left a comment
There was a problem hiding this comment.
I think this is good to go, from the point of view of Mathlib.
Member
Author
Thanks everybody that invested time on this PR. Awesome teamwork! |
This was referenced Jan 4, 2024
This was referenced Feb 17, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
7 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.