[Merged by Bors] - chore: delete >6 month old deprecations (2024-10 11-21)#24271
[Merged by Bors] - chore: delete >6 month old deprecations (2024-10 11-21)#24271Parcly-Taxel wants to merge 9 commits intomasterfrom
Conversation
PR summary 954f19f247
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Data.List.Flatten | 278 | 55 | -223 (-80.22%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Data.List.Flatten |
-223 |
Declarations diff
- ArzelaAscoli.compactSpace_of_closedEmbedding
- ArzelaAscoli.isCompact_closure_of_closedEmbedding
- ClosedEmbedding
- ClosedEmbedding.LindelofSpace
- ClosedEmbedding.compactSpace
- ClosedEmbedding.isCompact_preimage
- ClosedEmbedding.isLindelof_preimage
- ClosedEmbedding.locallyCompactSpace
- ClosedEmbedding.measurable
- ClosedEmbedding.measurableEmbedding
- ClosedEmbedding.nonLindelofSpace
- ClosedEmbedding.noncompactSpace
- ClosedEmbedding.normalSpace
- ClosedEmbedding.paracompactSpace
- ClosedEmbedding.quasiSober
- ClosedEmbedding.restrictPreimage
- ClosedEmbedding.sigmaCompactSpace
- ClosedEmbedding.t4Space
- ClosedEmbedding.tendsto_coLindelof
- ClosedEmbedding.tendsto_cocompact
- ClosedEmbedding.topologicalKrullDim_le
- ClosedEmbedding.weaklyLocallyCompactSpace
- ContDiffWithinAt.comp'
- ContDiffWithinAt.comp_of_mem
- ContDiffWithinAt.congr'
- ContDiffWithinAt.congr_of_eventually_eq'
- ContMDiff.of_comp_openEmbedding
- Continuous.closedEmbedding
- ContinuousWithinAt.congr_nhds
- ContinuousWithinAt.mono_of_mem
- Filter.EventuallyEq.contDiffWithinAt_iff
- Function.LeftInverse.closedEmbedding
- HasFDerivWithinAt.comp_of_mem
- Int.closedEmbedding_coe_rat
- IsClosed.closedEmbedding_subtype_val
- IsLocallyInjective_iff_openEmbedding
- IsOpen.openEmbedding_subtype_val
- IsUniformEmbedding.toClosedEmbedding
- LinearMap.closedEmbedding_of_injective
- ListBlank.bind
- ListBlank.bind_mk
- ListBlank.cons_bind
- Module.End.iSup_genEigenspace_restrict_eq_top
- Nat.closedEmbedding_coe_rat
- Nat.sum_eq_listSum
- OpenEmbedding
- OpenEmbedding.coborder_preimage
- OpenEmbedding.compatiblePreserving
- OpenEmbedding.continuous
- OpenEmbedding.continuousAt_iff
- OpenEmbedding.functor_isContinuous
- OpenEmbedding.functor_obj_injective
- OpenEmbedding.generalizingMap
- OpenEmbedding.isLocalHomeomorph
- OpenEmbedding.isOpenMap
- OpenEmbedding.isQuasiSeparated_iff
- OpenEmbedding.locPathConnectedSpace
- OpenEmbedding.locallyCompactSpace
- OpenEmbedding.locallyConnectedSpace
- OpenEmbedding.map_nhdsWithin_preimage_eq
- OpenEmbedding.map_nhds_eq
- OpenEmbedding.measurableEmbedding
- OpenEmbedding.open_iff_image_open
- OpenEmbedding.open_iff_preimage_open
- OpenEmbedding.prodMap
- OpenEmbedding.quasiSober
- OpenEmbedding.restrictPreimage
- OpenEmbedding.singleton_smoothManifoldWithCorners
- OpenEmbedding.tendsto_nhds_iff
- OpenEmbedding.tendsto_nhds_iff'
- Perm.bind_left
- QuasiSeparatedSpace.of_openEmbedding
- Quotient.coe_smul_out'
- Quotient.mk_smul_out'
- Quotient.out'RelEmbedding
- Scheme.restrictFunctor_map_app
- Scheme.restrictFunctor_map_app_aux
- Scheme.restrictFunctor_map_base
- Scheme.restrictFunctor_map_ofRestrict
- Scheme.restrictFunctor_map_ofRestrict_assoc
- Scheme.restrictIsoOfEq
- Scheme.restrictMapIso
- Scheme.restrictRestrict
- Scheme.restrictRestrict_hom_restrict
- Scheme.restrictRestrict_hom_restrict_assoc
- Scheme.restrictRestrict_inv_restrict_restrict
- Scheme.restrictRestrict_inv_restrict_restrict_assoc
- Set.restrictPreimage_closedEmbedding
- Set.restrictPreimage_openEmbedding
- Sigma.openEmbedding_ι
- StrictOrder.cof
- StrictOrder.cof_nonempty
- TopCat.Presheaf.isSheaf_of_openEmbedding
- ULift.closedEmbedding_down
- UniformEmbedding.toClosedEmbedding
- _root_.ClosedEmbedding.integral_map
- _root_.ClosedEmbedding.polishSpace
- _root_.ClosedEmbedding.setIntegral_map
- _root_.Embedding.toOpenEmbedding_of_surjective
- _root_.FiniteDimensional.finite_of_finite
- _root_.FreeAddMonoid.ofList_join
- _root_.InitialSeg.ltOrEq_apply_left
- _root_.QuotientGroup.out'_conj_pow_minimalPeriod_mem
- _root_.closedEmbedding_id
- _root_.closedEmbedding_of_continuous_injective_closed
- _root_.closedEmbedding_of_embedding_closed
- _root_.elementalStarAlgebra.closedEmbedding_coe
- _root_.openEmbedding_id
- add_isLimit
- add_isNormal
- add_pow_eq_add_pow_mod_mul_pow_add_pow_div
- adjoin_induction'
- adjoin_induction_subtype
- aemeasurable_biInf
- aemeasurable_biSup
- aemeasurable_iInf
- aemeasurable_iSup
- aleph'
- aleph'_cof
- aleph'_isNormal
- aleph'_le
- aleph'_le_of_limit
- aleph'_limit
- aleph'_lt
- aleph'_max
- aleph'_nat
- aleph'_omega0
- aleph'_pos
- aleph'_succ
- aleph'_zero
- aleph0_le_aleph'
- aleph_cof
- aleph_eq_aleph'
- aleph_isNormal
- aleph_le
- aleph_lt
- append_join_map_append
- apply_le_nfpBFamily
- apply_lt_nfpBFamily
- apply_lt_nfpBFamily_iff
- autEmbedding_closedEmbedding
- beth_normal
- binaryRec_eq'
- bind_append_perm
- bind_congr
- bind_eq_bind
- bind_pure_eq_map
- bit_eq_zero
- blsub₂
- cfcHom_closedEmbedding
- cfcₙHom_closedEmbedding
- chain'_join
- closedEmbedding_cfcAux
- closedEmbedding_cfcₙAux
- closedEmbedding_cfcₙHom_of_cfcHom
- closedEmbedding_coe_ennreal
- closedEmbedding_comap_of_surjective
- closedEmbedding_iff_closedEmbedding_of_iSup_eq_top
- closedEmbedding_inclusion
- closedEmbedding_inl
- closedEmbedding_inr
- closedEmbedding_mk
- closedEmbedding_mk_symm
- closedEmbedding_natUnionInftyEmbedding
- closedEmbedding_nonUnitalStarAlgHom
- closedEmbedding_of_pairwise_le_dist
- closedEmbedding_of_spaced_out
- closedEmbedding_sigmaMk
- closedEmbedding_smul_left
- closedEmbedding_starAlgHom
- closedEmbedding_subtype_val
- closedEmbedding_toContinuousMultilinearMap
- closedEmbedding_update
- closure_induction'
- coe_negOnePow
- cof_le
- compRightHomeomorph
- comp_closedEmbedding
- contMDiffOn_openEmbedding_symm
- contMDiff_openEmbedding
- continuousWithinAt_congr_nhds
- continuous_comp
- continuous_comp_left
- continuous_insertNth'
- countP_bind
- countP_bind'
- countP_flatMap'
- countP_flatten'
- count_bind
- count_bind'
- count_flatMap'
- count_flatten'
- derivBFamily
- derivBFamily_eq_derivFamily
- derivBFamily_eq_enumOrd
- derivBFamily_fp
- derivBFamily_isNormal
- derivBFamily_lt_ord
- derivBFamily_lt_ord_lift
- derivFamily_isNormal
- deriv_isNormal
- disjoint_out'
- drop_sum_flatten'
- drop_sum_join
- drop_take_succ_flatten_eq_getElem'
- drop_take_succ_join_eq_getElem'
- embedding_comp
- equivLT
- equivLT_apply
- equivLT_top
- eraseNth_val
- eta
- exists_aleph
- exists_extension_forall_exists_le_ge_of_closedEmbedding
- exists_extension_forall_mem_Icc_of_closedEmbedding
- exists_extension_norm_eq_of_closedEmbedding
- exists_extension_norm_eq_of_closedEmbedding'
- exists_extension_of_closedEmbedding
- exists_hasEigenvalue_of_iSup_genEigenspace_eq_top
- ext₃
- filterMap_eq_bind_toList
- finiteCoproduct.openEmbedding_ι
- flatten_drop_length_sub_one
- foldr_le_nfpBFamily
- fp_iff_derivBFamily
- fromGlued_openEmbedding
- fromOpenSubsetsGlue_openEmbedding
- fst_openEmbedding_of_right_openEmbedding
- getElem_insertNth_add_succ
- getElem_insertNth_of_lt
- getElem_insertNth_self
- get_insertNth_add_succ
- get_insertNth_of_lt
- get_insertNth_self
- iSup_genEigenspace_eq_top
- index_out'
- inducing_comp
- infix_bind_of_mem
- injOn_insertNth_index_of_not_mem
- insertNth
- insertNth_eraseIdx_of_ge
- insertNth_eraseIdx_of_le
- insertNth_injective
- insertNth_length_self
- insertNth_of_length_lt
- insertNth_succ_cons
- insertNth_succ_nil
- insertNth_val
- insertNth_zero
- integral_empty
- integral_union
- integral_univ
- isFiniteMeasure_sFiniteSeq
- isLocalHomeomorphOn_iff_openEmbedding_restrict
- isLocalHomeomorph_iff_openEmbedding_restrict
- isNormal_derivBFamily
- isOfFinOrder_one
- isProperMap_of_closedEmbedding
- isProperMap_restr_of_proper_of_closed
- isProperMap_subtype_val_of_closed
- isRegular_aleph'_succ
- isSeparatedMap_iff_closedEmbedding
- join_drop_length_sub_one
- join_splitBy
- join_splitWrtComposition
- join_splitWrtCompositionAux
- ker_apply_mk_out'
- leLT
- leLT_apply
- le_iff_derivBFamily
- le_nfpBFamily
- le_of_forall_pos_le_add
- length_bind
- length_bind'
- length_flatMap'
- length_flatten'
- length_insertNth
- length_insertNth_le_succ
- length_le_length_insertNth
- length_sigma'
- lift_aleph'
- list_bind
- list_join
- locPathConnected_of_bases
- locPathConnected_of_isOpen
- localization_away_openEmbedding
- ltEquiv
- ltLe
- ltOrEq
- ltOrEq_apply_right
- lt_blsub₂
- lt_le_apply
- lt_le_top
- lt_nfpBFamily
- mapIdxGo_length
- mapIdx_eq_nil
- map_append_bind_perm
- map_mk
- max_mul
- measurable_biInf
- measurable_biSup
- measurable_iInf
- measurable_iSup
- measurable_liminf
- measurable_liminf'
- measurable_limsup
- measurable_limsup'
- measurable_sInf
- measurable_sSup
- measurable_spanningSets
- mem_insertNth
- mk'_def
- modifyNthTail_modifyNthTail_le
- modifyNthTail_modifyNthTail_same
- modifyNth_eq_set
- mul_isLimit
- mul_isLimit_left
- mul_isNormal
- mul_left_mono
- mul_max
- mul_principal_add_is_principal_add
- mul_right_mono
- natCast_eq_zero
- natCast_injective
- natCast_ne_zero
- natCast_pos
- natCast_pow
- nfpBFamily
- nfpBFamily_eq_nfpFamily
- nfpBFamily_eq_self
- nfpBFamily_fp
- nfpBFamily_le
- nfpBFamily_le_apply
- nfpBFamily_le_fp
- nfpBFamily_le_iff
- nfpBFamily_lt_ord
- nfpBFamily_lt_ord_lift
- nfpBFamily_lt_ord_lift_of_isRegular
- nfpBFamily_lt_ord_of_isRegular
- nfpBFamily_monotone
- nfpFamily_eq_sup
- nodupKeys_join
- normalize_monic
- not_bddAbove_fp_bfamily
- ofList_join
- ofNat''
- ofReal'
- omega0_isLimit
- omega_lt_omega1
- openEmbedding'
- openEmbedding_exp
- openEmbedding_iff_comp_isIso
- openEmbedding_iff_comp_isIso'
- openEmbedding_iff_continuous_injective_open
- openEmbedding_iff_embedding_open
- openEmbedding_iff_isIso_comp
- openEmbedding_iff_isIso_comp'
- openEmbedding_iff_openEmbedding_of_iSup_eq_top
- openEmbedding_inl
- openEmbedding_inr
- openEmbedding_mk
- openEmbedding_natCast
- openEmbedding_obj_top
- openEmbedding_of_comp
- openEmbedding_of_embedding_open
- openEmbedding_of_injective
- openEmbedding_of_le
- openEmbedding_of_pullback_open_embeddings
- openEmbedding_restrict
- openEmbedding_sigmaMk
- openEmbedding_sigma_map
- openEmbedding_val
- opow_isLimit
- opow_isLimit_left
- opow_isNormal
- opow_principal_add_of_principal_add
- orbitRel_r_apply
- orbit_eq_out'_smul
- ord_aleph_isLimit
- ord_isLimit
- out'
- perm_option_to_list
- pow_strictMono
- power_cast_right
- preAleph_cof
- preAleph_isNormal
- principal_add_isLimit
- principal_mul_isLimit
- principal_nfp_blsub₂
- prod_join
- properSMul_of_closedEmbedding
- pullbackRestrictIsoRestrict_hom_restrict
- pullbackRestrictIsoRestrict_hom_restrict_assoc
- pullback_map_openEmbedding_of_open_embeddings
- ranges_flatten'
- ranges_join
- ranges_join'
- removeNth_insertIdx
- sFiniteSeq
- sFiniteSeq_absolutelyContinuous_toFinite
- sFiniteSeq_le
- sFiniteSeq_zero
- separated_by_openEmbedding
- setIntegral_congr
- setIntegral_congr_set_ae
- setIntegral_congr₀
- sigma_ι_openEmbedding
- smul_set_disjoint_iff
- snd_openEmbedding_of_left_openEmbedding
- splitWrtComposition_join
- stalkPushforward_iso_of_openEmbedding
- sub_isLimit
- sublistsAux_eq_bind
- sum_join
- sum_sFiniteSeq
- take_sum_flatten'
- take_sum_join
- tendsto_insertNth'
- toContinuousMap
- to_openEmbedding
- totalSpaceMk_closedEmbedding
- type_def
- type_def'
- type_lift_preimage_aux
- type_lt
- unbounded_principal
-- closedEmbedding_coe_real
-- closedEmbedding_toContinuousMap
-- continuous_insertNth
-- empty_nsmul
-- exists_extension_forall_mem_of_closedEmbedding
-- insertNth_comm
-- lift_umax'
-- mk_out'_eq_mul
-- natCast_inj
-- natCast_le
-- natCast_lt
-- tendsto_insertNth
-- ι_openEmbedding
---- openEmbedding_coe
----- openEmbedding
------- closedEmbedding
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.
Decrease in tech debt: (relative, absolute) = (5.00, 0.07)
| Current number | Change | Type |
|---|---|---|
| 69 | -5 | disabled deprecation lints |
Current commit 954f19f247
Reference commit 26979609f2
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
There was a problem hiding this comment.
Thanks!
In the future, could we please have the regex automatically run, the changes committed and the PR approved by a bot (akin to the nolints update)? That way, your PRs would only need to deal with the manual cleanups (and be much faster to review!).
maintainer merge
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
Vierkantor
left a comment
There was a problem hiding this comment.
I checked everything else and it looks good to me. Thanks! 🎉
bors d+
|
✌️ Parcly-Taxel can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
The first commit was done automatically using #21271's method, with the regex ``` @\[deprecated.*\(since := "2024-10-([01].|2[01])"\)\][\s\n]?(protected )?alias [_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟'.₀₁₂₃₄₅₆₇₈₉]* :=[\s\n]+[_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟'.₀₁₂₃₄₅₆₇₈₉]*\n\n? ``` The remaining commits are manual removals of empty sections and missed deprecations (`2024-10-([01].|2[01])`).
|
Pull request successfully merged into master. Build succeeded: |
The first commit was done automatically using #21271's method, with the regex ``` @\[deprecated.*\(since := "2024-10-([01].|2[01])"\)\][\s\n]?(protected )?alias [_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟'.₀₁₂₃₄₅₆₇₈₉]* :=[\s\n]+[_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟'.₀₁₂₃₄₅₆₇₈₉]*\n\n? ``` The remaining commits are manual removals of empty sections and missed deprecations (`2024-10-([01].|2[01])`).
The first commit was done automatically using #21271's method, with the regex
The remaining commits are manual removals of empty sections and missed deprecations (
2024-10-([01].|2[01])).