Aesop forward benchmark: forward no-precomp#21609
Draft
Aesop forward benchmark: forward no-precomp#21609
Conversation
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Johan Commelin <johan@commelin.net>
Collaborator
Author
|
!bench |
PR summary 6eb30988f5Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
Collaborator
|
Here are the benchmark results for commit 6eb3098. Benchmark Metric Change
=============================================================================================
- build aesop 50.8%
- ~Aesop.RuleSet instructions 88.0%
- ~Aesop.Search.Main instructions 151.3%
+ ~Batteries.Data.Array.Lemmas instructions -91.9%
- ~Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital instructions 4.9%
- ~Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order instructions 13.8%
- ~Mathlib.Analysis.Convex.Visible instructions 36.6%
- ~Mathlib.CategoryTheory.ComposableArrows instructions 4.7%
- ~Mathlib.CategoryTheory.Limits.Cones instructions 3.4%
- ~Mathlib.CategoryTheory.Triangulated.Functor instructions 8.3%
- ~Mathlib.CategoryTheory.Triangulated.TriangleShift instructions 11.0%
- ~Mathlib.CategoryTheory.WithTerminal instructions 8.8%
- ~Mathlib.LinearAlgebra.QuadraticForm.TensorProduct instructions 11.0%
- ~Mathlib.Probability.Kernel.Proper instructions 113.7%
- ~Mathlib.Tactic.Module instructions 9.1% |
2 files, Instructions +14.0⬝10⁹
2 files, Instructions +11.0⬝10⁹
2 files, Instructions +10.0⬝10⁹
2 files, Instructions +9.0⬝10⁹
2 files, Instructions +8.0⬝10⁹
6 files, Instructions +7.0⬝10⁹
4 files, Instructions +6.0⬝10⁹
9 files, Instructions +5.0⬝10⁹
16 files, Instructions +4.0⬝10⁹
23 files, Instructions +3.0⬝10⁹
67 files, Instructions +2.0⬝10⁹
168 files, Instructions +1.0⬝10⁹
4 files, Instructions -2.0⬝10⁹
2 files, Instructions -3.0⬝10⁹
|
leanprover-community-bot-assistant
added
the
merge-conflict
Collaborator
Author
|
!bench |
Collaborator
|
Here are the benchmark results for commit 6aba2b2. Benchmark Metric Change
=============================================================================================
- build aesop 48.2%
- ~Aesop.RuleSet instructions 88.0%
- ~Aesop.Search.Main instructions 151.3%
+ ~Batteries.Data.Array.Lemmas instructions -91.9%
- ~Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital instructions 4.9%
- ~Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order instructions 13.8%
- ~Mathlib.Analysis.Convex.Visible instructions 36.6%
- ~Mathlib.CategoryTheory.ComposableArrows instructions 4.7%
- ~Mathlib.CategoryTheory.Limits.Cones instructions 3.4%
- ~Mathlib.CategoryTheory.Triangulated.Functor instructions 8.3%
- ~Mathlib.CategoryTheory.Triangulated.TriangleShift instructions 11.0%
- ~Mathlib.CategoryTheory.WithTerminal instructions 8.8%
- ~Mathlib.LinearAlgebra.QuadraticForm.TensorProduct instructions 11.0%
- ~Mathlib.Probability.Kernel.Proper instructions 113.7%
- ~Mathlib.Tactic.Module instructions 9.1% |
2 files, Instructions +14.0⬝10⁹
2 files, Instructions +11.0⬝10⁹
2 files, Instructions +10.0⬝10⁹
2 files, Instructions +9.0⬝10⁹
3 files, Instructions +8.0⬝10⁹
5 files, Instructions +7.0⬝10⁹
4 files, Instructions +6.0⬝10⁹
9 files, Instructions +5.0⬝10⁹
16 files, Instructions +4.0⬝10⁹
23 files, Instructions +3.0⬝10⁹
67 files, Instructions +2.0⬝10⁹
168 files, Instructions +1.0⬝10⁹
4 files, Instructions -2.0⬝10⁹
2 files, Instructions -3.0⬝10⁹
|
This is for the rule pattern indexing optimisation.
Collaborator
Author
|
!bench |
Collaborator
|
Here are the benchmark results for commit 1deef08. Benchmark Metric Change
=========================================================================================
- build aesop 15.8%
- ~Aesop.RuleSet instructions 88.0%
- ~Aesop.Search.Main instructions 151.3%
+ ~Batteries.Data.Array.Lemmas instructions -91.9%
- ~Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order instructions 13.5%
- ~Mathlib.Analysis.Convex.Visible instructions 36.0%
- ~Mathlib.CategoryTheory.Triangulated.Functor instructions 5.1%
- ~Mathlib.LinearAlgebra.QuadraticForm.TensorProduct instructions 10.7%
- ~Mathlib.Probability.Kernel.Proper instructions 113.0%
- ~Mathlib.Tactic.Module instructions 9.1% |
2 files, Instructions +8.0⬝10⁹
3 files, Instructions +7.0⬝10⁹
5 files, Instructions +6.0⬝10⁹
3 files, Instructions +5.0⬝10⁹
11 files, Instructions +4.0⬝10⁹
5 files, Instructions +3.0⬝10⁹
28 files, Instructions +2.0⬝10⁹
66 files, Instructions +1.0⬝10⁹
17 files, Instructions -2.0⬝10⁹
7 files, Instructions -3.0⬝10⁹
4 files, Instructions -4.0⬝10⁹
4 files, Instructions -5.0⬝10⁹
|
Collaborator
Author
|
!bench |
Collaborator
|
Here are the benchmark results for commit 23a3c99. Benchmark Metric Change
====================================================
- build aesop 9.4%
- ~Aesop.RuleSet instructions 88.0%
- ~Aesop.Search.Main instructions 151.3%
+ ~Batteries.Data.Array.Lemmas instructions -91.9%
- ~Mathlib.Tactic.Module instructions 9.1% |
3 files, Instructions +7.0⬝10⁹
2 files, Instructions +6.0⬝10⁹
8 files, Instructions +4.0⬝10⁹
2 files, Instructions +3.0⬝10⁹
25 files, Instructions +2.0⬝10⁹
62 files, Instructions +1.0⬝10⁹
18 files, Instructions -2.0⬝10⁹
7 files, Instructions -3.0⬝10⁹
4 files, Instructions -4.0⬝10⁹
5 files, Instructions -5.0⬝10⁹
|
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
10 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.
Not a real PR, just for benchmarking.