[Merged by Bors] - perf: remove some with instance construction patterns#6241
Closed
mattrobball wants to merge 30 commits intomasterfrom
Closed
[Merged by Bors] - perf: remove some with instance construction patterns#6241mattrobball wants to merge 30 commits intomasterfrom
with instance construction patterns#6241mattrobball wants to merge 30 commits intomasterfrom
Conversation
…' into mrb/kaehler_speedup
The optional fields to the algebra typeclasses are a trap; if you forget to provide them then you get diamonds.
Contributor
Author
|
!bench |
with instance construction patterns
Collaborator
|
Here are the benchmark results for commit 42ced2f.Found no runs to compare against. |
Member
|
Before we merge, I'll add an explanation to the PR description of why I think this happens. |
Member
|
bors d+ Please check you agree with the description before merging. I added myself as a co-author since I think the explanation is almost as important as the change here Though the change really is excellent! |
|
✌️ mattrobball can now approve this pull request. To approve and merge a pull request, simply reply with |
Member
|
!bench |
Collaborator
|
Here are the benchmark results for commit 42ced2f. Benchmark Metric Change
================================================================================
+ build .olean serialization -6.9%
+ build aesop -10.6%
+ build compilation -16.2%
+ build compilation new -10.9%
+ build elaboration -18.1%
+ build import -12.3%
+ build initialization -16.0%
+ build interpretation -16.3%
+ build linting -17.8%
+ build parsing -12.9%
+ build simp -17.6%
+ build tactic execution -21.1%
+ build task-clock -18.7%
+ build type checking -17.8%
+ build typeclass inference -21.4%
+ build wall-clock -19.6%
+ lint wall-clock -24.6%
- ~Mathlib.Algebra.Category.ModuleCat.Abelian instructions 5.7%
- ~Mathlib.Algebra.Category.ModuleCat.Limits instructions 15.7%
+ ~Mathlib.FieldTheory.Finite.GaloisField instructions -5.2%
+ ~Mathlib.FieldTheory.Normal instructions -9.1%
+ ~Mathlib.FieldTheory.PolynomialGaloisGroup instructions -10.4%
+ ~Mathlib.FieldTheory.SplittingField.Construction instructions -10.9%
+ ~Mathlib.MeasureTheory.Group.AddCircle instructions -6.0%
+ ~Mathlib.RingTheory.Polynomial.GaussLemma instructions -10.7% |
Member
|
(the previous benchmark apparently might be bogus) |
Contributor
Author
|
So I guess it caches the runs? |
Member
|
Seems so; I've asked it to discard the last run |
Member
|
!bench |
Collaborator
|
Here are the benchmark results for commit 42ced2f. Benchmark Metric Change
================================================================================
+ build .olean serialization -6.9%
+ build aesop -10.6%
+ build compilation -16.2%
+ build compilation new -10.9%
+ build elaboration -18.1%
+ build import -12.3%
+ build initialization -16.0%
+ build interpretation -16.3%
+ build linting -17.8%
+ build parsing -12.9%
+ build simp -17.6%
+ build tactic execution -21.1%
+ build task-clock -18.7%
+ build type checking -17.8%
+ build typeclass inference -21.4%
+ build wall-clock -19.6%
+ lint wall-clock -24.6%
- ~Mathlib.Algebra.Category.ModuleCat.Abelian instructions 5.7%
- ~Mathlib.Algebra.Category.ModuleCat.Limits instructions 15.7%
+ ~Mathlib.FieldTheory.Finite.GaloisField instructions -5.2%
+ ~Mathlib.FieldTheory.Normal instructions -9.1%
+ ~Mathlib.FieldTheory.PolynomialGaloisGroup instructions -10.4%
+ ~Mathlib.FieldTheory.SplittingField.Construction instructions -10.9%
+ ~Mathlib.MeasureTheory.Group.AddCircle instructions -6.0%
+ ~Mathlib.RingTheory.Polynomial.GaussLemma instructions -10.7% |
Collaborator
|
Here are the benchmark results for commit 42ced2f. Benchmark Metric Change
========================================================================
- ~Mathlib.Algebra.Category.ModuleCat.Abelian instructions 5.7%
- ~Mathlib.Algebra.Category.ModuleCat.Limits instructions 15.7%
+ ~Mathlib.FieldTheory.Finite.GaloisField instructions -5.2%
+ ~Mathlib.FieldTheory.Normal instructions -9.1%
+ ~Mathlib.FieldTheory.PolynomialGaloisGroup instructions -10.4%
+ ~Mathlib.FieldTheory.SplittingField.Construction instructions -10.9%
+ ~Mathlib.MeasureTheory.Group.AddCircle instructions -6.0%
+ ~Mathlib.RingTheory.Polynomial.GaussLemma instructions -10.7% |
Contributor
Author
|
That is what I expect |
Member
|
I think this is probably still worth merging; do you agree? |
Contributor
Author
|
Do you want to amend? |
Contributor
Author
|
Oh already done. |
Contributor
Author
|
bors merge |
bors bot
pushed a commit
that referenced
this pull request
Aug 2, 2023
The general thought here is that
```lean
{ hf.distribMulAction f smul with
smul := (· • ·)
... }
```
is treated roughly as
```lean
let src := hf.distribMulAction f smul
{ toDistribMulAction :=
{ toMulAction :=
{ smul := (· • ·)
one_smul := src.one_smul
mul_smul := src.mul_smul}
smul_add := src.smul_add
smul_zero := src.smul_zero }
... }
```
which is a much larger term (especially once the `let` is reduced, due to how many arguments `hf.distribMulAction` consumes) than
```lean
{ toDistribMulAction := hf.distribMulAction f smul
... }
```
In some places the long version is _maybe_ still more desirable, if we want a specific syntactic equality for `smul` that the base structure defines differently; but none of the examples in this PR are such a case.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Matthew Ballard <matt@mrb.email>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
with instance construction patternswith instance construction patterns
kim-em
pushed a commit
that referenced
this pull request
Aug 2, 2023
The general thought here is that
```lean
{ hf.distribMulAction f smul with
smul := (· • ·)
... }
```
is treated roughly as
```lean
let src := hf.distribMulAction f smul
{ toDistribMulAction :=
{ toMulAction :=
{ smul := (· • ·)
one_smul := src.one_smul
mul_smul := src.mul_smul}
smul_add := src.smul_add
smul_zero := src.smul_zero }
... }
```
which is a much larger term (especially once the `let` is reduced, due to how many arguments `hf.distribMulAction` consumes) than
```lean
{ toDistribMulAction := hf.distribMulAction f smul
... }
```
In some places the long version is _maybe_ still more desirable, if we want a specific syntactic equality for `smul` that the base structure defines differently; but none of the examples in this PR are such a case.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Matthew Ballard <matt@mrb.email>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
kim-em
pushed a commit
that referenced
this pull request
Aug 2, 2023
The general thought here is that
```lean
{ hf.distribMulAction f smul with
smul := (· • ·)
... }
```
is treated roughly as
```lean
let src := hf.distribMulAction f smul
{ toDistribMulAction :=
{ toMulAction :=
{ smul := (· • ·)
one_smul := src.one_smul
mul_smul := src.mul_smul}
smul_add := src.smul_add
smul_zero := src.smul_zero }
... }
```
which is a much larger term (especially once the `let` is reduced, due to how many arguments `hf.distribMulAction` consumes) than
```lean
{ toDistribMulAction := hf.distribMulAction f smul
... }
```
In some places the long version is _maybe_ still more desirable, if we want a specific syntactic equality for `smul` that the base structure defines differently; but none of the examples in this PR are such a case.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Matthew Ballard <matt@mrb.email>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
kim-em
pushed a commit
that referenced
this pull request
Aug 3, 2023
The general thought here is that
```lean
{ hf.distribMulAction f smul with
smul := (· • ·)
... }
```
is treated roughly as
```lean
let src := hf.distribMulAction f smul
{ toDistribMulAction :=
{ toMulAction :=
{ smul := (· • ·)
one_smul := src.one_smul
mul_smul := src.mul_smul}
smul_add := src.smul_add
smul_zero := src.smul_zero }
... }
```
which is a much larger term (especially once the `let` is reduced, due to how many arguments `hf.distribMulAction` consumes) than
```lean
{ toDistribMulAction := hf.distribMulAction f smul
... }
```
In some places the long version is _maybe_ still more desirable, if we want a specific syntactic equality for `smul` that the base structure defines differently; but none of the examples in this PR are such a case.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Matthew Ballard <matt@mrb.email>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
kim-em
pushed a commit
that referenced
this pull request
Aug 14, 2023
The general thought here is that
```lean
{ hf.distribMulAction f smul with
smul := (· • ·)
... }
```
is treated roughly as
```lean
let src := hf.distribMulAction f smul
{ toDistribMulAction :=
{ toMulAction :=
{ smul := (· • ·)
one_smul := src.one_smul
mul_smul := src.mul_smul}
smul_add := src.smul_add
smul_zero := src.smul_zero }
... }
```
which is a much larger term (especially once the `let` is reduced, due to how many arguments `hf.distribMulAction` consumes) than
```lean
{ toDistribMulAction := hf.distribMulAction f smul
... }
```
In some places the long version is _maybe_ still more desirable, if we want a specific syntactic equality for `smul` that the base structure defines differently; but none of the examples in this PR are such a case.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Matthew Ballard <matt@mrb.email>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
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
4 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.
The general thought here is that
{ hf.distribMulAction f smul with smul := (· • ·) ... }is treated roughly as
let src := hf.distribMulAction f smul { toDistribMulAction := { toMulAction := { smul := (· • ·) one_smul := src.one_smul mul_smul := src.mul_smul} smul_add := src.smul_add smul_zero := src.smul_zero } ... }which is a much larger term (especially once the
letis reduced, due to how many argumentshf.distribMulActionconsumes) than{ toDistribMulAction := hf.distribMulAction f smul ... }In some places the long version is maybe still more desirable, if we want a specific syntactic equality for
smulthat the base structure defines differently; but none of the examples in this PR are such a case.Co-authored-by: Eric Wieser wieser.eric@gmail.com