[Merged by Bors] - chore: bump toolchain to v4.3.0-rc1 #8051
Conversation
This file contains 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
semorrison
added
awaiting-review
leanprover-community-mathlib4-bot
added
blocked-by-other-PR
|
This PR/issue depends on: |
|
!bench |
eric-wieser
reviewed
Oct 31, 2023
eric-wieser
reviewed
Oct 31, 2023
| @@ -155,7 +155,8 @@ theorem cutMap_add (a b : α) : cutMap β (a + b) = cutMap β a + cutMap β b := | |||
| rw [coe_mem_cutMap_iff] | |||
| exact_mod_cast sub_lt_comm.mp hq₁q | |||
| · rintro _ ⟨_, _, ⟨qa, ha, rfl⟩, ⟨qb, hb, rfl⟩, rfl⟩ | |||
| refine' ⟨qa + qb, _, by norm_cast⟩ | |||
| -- After leanprover/lean4#2734, `norm_cast` needs help with beta reduction. | |||
There was a problem hiding this comment.
This looks like a possibly regression to me (and the only one in this patch); can you explain what's going on in the PR description, and maybe open a tracking issue for fixing this to be referenced there too?
There was a problem hiding this comment.
Tracking issue at #8052.
(Also, since you read these diffs I've changed these regressions to use beta_reduce or unfold_let specifically, instead of a blind dsimp.)
|
Here are the benchmark results for commit ec994a6. |
leanprover-community-mathlib4-bot
added
the
merge-conflict
semorrison
removed
the
merge-conflict
|
!bench |
|
Here are the benchmark results for commit eb549bf. Benchmark Metric Change
===========================================================================
- ~Mathlib.Algebra.Module.LocalizedModule instructions 2.8%
+ ~Mathlib.CategoryTheory.Abelian.InjectiveResolution instructions -1.5%
+ ~Mathlib.CategoryTheory.Abelian.Projective instructions -2.3%
- ~Mathlib.CategoryTheory.Functor.Flat instructions 182.6%
- ~Mathlib.CategoryTheory.Monoidal.Mon_ instructions 3.8%
- ~Mathlib.FieldTheory.RatFunc instructions 2.5%
- ~Mathlib.LinearAlgebra.FinsuppVectorSpace instructions 3.0%
+ ~Mathlib.NumberTheory.NumberField.Units instructions -3.1% |
|
Ouch, what happened to |
eric-wieser
reviewed
Oct 31, 2023
Mathlib/Data/Complex/Module.lean
Outdated
| @@ -481,7 +481,7 @@ lemma IsSelfAdjoint.coe_realPart {x : A} (hx : IsSelfAdjoint x) : | |||
|
|
|||
| lemma IsSelfAdjoint.imaginaryPart {x : A} (hx : IsSelfAdjoint x) : | |||
| ℑ x = 0 := by | |||
| rw [imaginaryPart, LinearMap.comp_apply, hx.skewAdjointPart_apply _, map_zero] | |||
| rw [_root_.imaginaryPart, LinearMap.comp_apply, hx.skewAdjointPart_apply _, map_zero] | |||
There was a problem hiding this comment.
This isn't the same thing as was in #7872... I'll push a fix.
leanprover-community-mathlib4-bot
added
the
ready-to-merge
leanprover-community-mathlib4-bot
removed
the
awaiting-review
|
bors p=10 |
|
bors single on |
bors bot
pushed a commit
that referenced
this pull request
Oct 31, 2023
This incorporates changes from * #7845 * #7847 * #7853 * #7872 (was never actually made to work, but the diffs in `nightly-testing` are unexciting: we need to fully qualify a few names) They can all be closed when this is merged. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> 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. |
bors
bot
changed the title
bors bot
pushed a commit
that referenced
this pull request
Oct 31, 2023
This file recently jumped almost 200% in #8051. Changing a `simpa using X` call into a `convert X <;> simp` cuts the clock time for the file in half.
bors bot
pushed a commit
that referenced
this pull request
Oct 31, 2023
This file recently jumped almost 200% in #8051. Changing a `simpa using X` call into a `convert X <;> simp` cuts the clock time for the file in half.
This was referenced Oct 31, 2023
fgdorais
pushed a commit
that referenced
this pull request
Nov 1, 2023
This incorporates changes from * #7845 * #7847 * #7853 * #7872 (was never actually made to work, but the diffs in `nightly-testing` are unexciting: we need to fully qualify a few names) They can all be closed when this is merged. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
fgdorais
pushed a commit
that referenced
this pull request
Nov 1, 2023
This file recently jumped almost 200% in #8051. Changing a `simpa using X` call into a `convert X <;> simp` cuts the clock time for the file in half.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
This incorporates changes from
nightly-testingare unexciting: we need to fully qualify a few names)They can all be closed when this is merged.
Once the std PR is merged, we need to change the
lakefile.leanhere to point back tomain. ✅