[Merged by Bors] - chore: adaptations for nightly-2024-11-14 #19059
Conversation
PR summary 289565489b
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Data.DFinsupp.Sigma | 564 | 562 | -2 (-0.35%) |
| Mathlib.MeasureTheory.MeasurableSpace.Embedding | 652 | 650 | -2 (-0.31%) |
| Mathlib.Algebra.Category.Ring.Epi | 1124 | 1122 | -2 (-0.18%) |
| Mathlib.RingTheory.Polynomial.UniqueFactorization | 1132 | 1130 | -2 (-0.18%) |
| Mathlib.MeasureTheory.Group.Measure | 1341 | 1340 | -1 (-0.07%) |
| Mathlib.Algebra.Lie.Semisimple.Basic | 1344 | 1343 | -1 (-0.07%) |
| Mathlib.FieldTheory.Relrank | 1377 | 1376 | -1 (-0.07%) |
| Mathlib.RingTheory.Jacobson | 1395 | 1394 | -1 (-0.07%) |
| Mathlib.FieldTheory.KummerExtension | 1441 | 1440 | -1 (-0.07%) |
| Mathlib.Geometry.Manifold.Instances.Real | 1792 | 1791 | -1 (-0.06%) |
| Mathlib.Analysis.Complex.UpperHalfPlane.Metric | 1820 | 1819 | -1 (-0.05%) |
| Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order | 2150 | 2149 | -1 (-0.05%) |
Import changes for all files
| Files | Import difference |
|---|---|
| There are 3614 files with changed transitive imports taking up over 156170 characters: this is too many to display! | |
You can run scripts/import_trans_difference.sh all locally to see the whole output. |
Declarations diff
+ getLast_filter'
+ subset_of_le
+ zero
- eraseIdx_insertIdx
- find?_eq_some_iff_getElem
- getElem_insertIdx_of_lt
- getElem_insertIdx_self
- getLast_filter
- getLast_ofFn
- head_ofFn
- insertIdx_comm
- insertIdx_eraseIdx_of_ge
- insertIdx_eraseIdx_of_le
- insertIdx_length_self
- insertIdx_of_length_lt
- insertIdx_succ_cons
- insertIdx_succ_nil
- insertIdx_zero
- length_insertIdx
- length_insertIdx_le_succ
- length_le_length_insertIdx
- mapIdxGo_append
- mem_insertIdx
- modifyNthTail_modifyNthTail
- modifyTailIdx_modifyTailIdx
- modifyTailIdx_modifyTailIdx_le
- modifyTailIdx_modifyTailIdx_same
- ofFn_eq_nil_iff
- ofFn_succ
- ofFn_zero
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 script/declarations_diff.sh contains some details about this script.
Increase in tech debt: 4.79
| Current number | Change | Type |
|---|---|---|
| 5086 | -11 | porting notes |
| 189 | 4 | adaptation notes |
| 224 | 4 | disabled simpNF lints |
| 1555 | -2 | erw |
| 14 | 5 | maxHeartBeats modifications |
Current commit 289565489b
Reference commit daed990be8
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
| @@ -24,7 +24,7 @@ lemma CommRingCat.epi_iff_tmul_eq_tmul {R S : Type u} [CommRing R] [CommRing S] | |||
| constructor | |||
| · intro H | |||
| have := H.1 (CommRingCat.ofHom <| Algebra.TensorProduct.includeLeftRingHom (R := R)) | |||
| (CommRingCat.ofHom <| Algebra.TensorProduct.includeRight.toRingHom) | |||
| (CommRingCat.ofHom <| (Algebra.TensorProduct.includeRight (R := R) (A := S)).toRingHom) | |||
There was a problem hiding this comment.
This makes me a little bit sad, but we can certainly live with this.
| @@ -212,7 +212,7 @@ lemma finitelyAtomistic : ∀ s : Finset (LieIdeal R L), ↑s ⊆ {I : LieIdeal | |||
| set K := s'.sup id | |||
| suffices I ≤ K by | |||
| obtain ⟨t, hts', htI⟩ := finitelyAtomistic s' hs'S I this | |||
| exact ⟨t, hts'.trans hs'.subset, htI⟩ | |||
| exact ⟨t, Finset.Subset.trans hts' hs'.subset, htI⟩ | |||
There was a problem hiding this comment.
Do we understand this regression? This makes me moderately sad...
| @@ -63,14 +63,14 @@ theorem sigmaCurry_zero [∀ i j, Zero (δ i j)] : | |||
|
|
|||
| @[simp] | |||
| theorem sigmaCurry_add [∀ i j, AddZeroClass (δ i j)] (f g : Π₀ (i : Σ _, _), δ i.1 i.2) : | |||
| sigmaCurry (f + g) = sigmaCurry f + sigmaCurry g := by | |||
| sigmaCurry (f + g) = (sigmaCurry f + sigmaCurry g : Π₀ (i) (j), δ i j) := by | |||
There was a problem hiding this comment.
This makes me a little bit sad, but I guess it's not too bad.
| @@ -35,11 +35,13 @@ variable {E : Type v} [Field E] {L : Type w} [Field L] | |||
|
|
|||
| variable (A B C : Subfield E) | |||
|
|
|||
| set_option synthInstance.maxHeartbeats 400000 in | |||
There was a problem hiding this comment.
Can we add some adaptation notes here? Or is this just a fact of life that we have to live with until we debug/speedup?
| @@ -764,7 +764,7 @@ nonrec theorem _root_.MulEquiv.isHaarMeasure_map [BorelSpace G] [TopologicalGrou | |||
| [TopologicalGroup H] (e : G ≃* H) (he : Continuous e) (hesymm : Continuous e.symm) : | |||
| IsHaarMeasure (Measure.map e μ) := | |||
| let f : G ≃ₜ H := .mk e | |||
| isHaarMeasure_map μ e he e.surjective f.isClosedEmbedding.tendsto_cocompact | |||
| isHaarMeasure_map μ e.toMonoidHom he e.surjective f.isClosedEmbedding.tendsto_cocompact | |||
There was a problem hiding this comment.
Why do we need this now? Makes me mildly sad.
| @@ -507,8 +507,10 @@ def arrowProdEquivProdArrow (α β γ : Type*) [MeasurableSpace α] [MeasurableS | |||
| measurable_toFun _ h := by | |||
| simp_rw [Equiv.arrowProdEquivProdArrow, coe_fn_mk] | |||
| exact MeasurableSet.preimage h (Measurable.prod_mk | |||
| (measurable_pi_lambda (fun a c ↦ (a c).1) fun a ↦ (measurable_pi_apply a).fst) | |||
| (measurable_pi_lambda (fun a c ↦ (a c).2) fun a ↦ (measurable_pi_apply a).snd )) | |||
| (measurable_pi_lambda (fun (a : γ → α × β) c ↦ (a c).1) | |||
There was a problem hiding this comment.
This becomes quite a bit more unreadable... mildly sad...
| @@ -704,7 +704,7 @@ lemma finite_of_finite_type_of_isJacobsonRing (R S : Type*) [CommRing R] [Field | |||
| obtain ⟨ι, hι, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial'.mp ‹_› | |||
| have : (algebraMap R S).IsIntegral := by | |||
| rw [← f.comp_algebraMap] | |||
| exact MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing f hf | |||
| exact MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing f.toRingHom hf | |||
|
These changes are sometimes regressions, but it's not like we don't have plenty of other occurrences of bors d+ |
|
✌️ kim-em can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Nearly all of the regressions are due to a horrible bug that Kyle discovered and fixed in leanprover/lean4#6024. Strangely, this bug was actually a helpful bug, that was conveying type hints into some unification problems, but via a really terrible mechanism. Kyle is thinking about ways we could improve the situation, but the squashing the bug is essential. |
|
I've added adaptation notes for all of the regressions Johan noted above. (Note there were already many backported to master in #18896, but I think these all had good notes already.) |
|
bors merge |
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com>
|
Pull request successfully merged into bump/v4.15.0. Build succeeded: |
mathlib-bors
bot
changed the title
I failed to push a local commit before sending #19059 to bors. Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com>
No description provided.