chore: adaptations for nightly-2025-03-28#23400
Conversation
PR summary 68f709d323
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Data.List.Sigma | 362 | 363 | +1 (+0.28%) |
| Mathlib.Data.List.AList | 363 | 364 | +1 (+0.28%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Data.List.AList Mathlib.Data.List.Sigma |
1 |
Declarations diff
+ bind_congr''
+ rootHashGeneration
+ toNat_lt''
- Lex.cons_iff
- add_div
- bind_congr
- ediv_emod_unique'
- emod_eq_add_self_emod
- emod_lt
- eq_or_lt_of_le
- ge_of_eq
- le_of_eq
- le_of_mul_le_mul_right
- le_or_lt
- le_rfl
- lt_iff_le_and_ne
- lt_of_le_of_lt
- lt_of_lt_of_le
- lt_or_eq_of_le
- lt_or_le
- lt_or_lt_of_ne
- mul_mod_mod
- natAbs_ediv
- natCast_succ
- toNat_le
- toNat_le_toNat
- toNat_lt'
- toNat_lt_toNat
- zero_le_ofNat
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: (relative, absolute) = (2.91, 0.49)
| Current number | Change | Type |
|---|---|---|
| 100 | 8 | adaptation notes |
| 62 | -1 | disabled simpNF lints |
| 7 | 3 | maxHeartBeats modifications |
Current commit 68f709d323
Reference commit 5626968096
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.
For anyone else wanting to look through this: the vast majority of changes are just caused by changes in explicitness of arguments (typically for list lemmas), and of these, the vast majority of these changes are removals of _ or named variable inputs, with a far smaller number of additions of (l := ...), so these look great.
On top of that there seemed to be only two other changes: firstly Data.Fin.Basic and Data.Int.Init had some lemmas removed (and my instinct with changes such as this are "if mathlib still compiles then probably this is fine" although Eric has in the past voiced some concerns about there being no automated check that some lemmas aren't being accidentally lost), and then there are small changes to two files in the Cache directory which I am not competent to comment on. So other than those two Cache changes (and a couple of other minor nits which I flag with comments above), LGTM.
YaelDillies
left a comment
There was a problem hiding this comment.
I am basing this review on my (currently unpublished) implicitness guide. According to it, there are a few very good changes to lemmas which are widely used, but also a lot of bad changes to less common lemmas.
I got bored after the 70th file, but hopefully you get the gist.
| simp [List.getElem_zero, head_first_row, hr] at h | ||
| simp_rw [cells.find?_eq_head_dropWhile_not hd, Option.get_some] | ||
| rw [← cells.takeWhile_append_dropWhile (fun c ↦ ! decide (r ≤ c.1)), | ||
| rw [← cells.takeWhile_append_dropWhile (p := fun c ↦ ! decide (r ≤ c.1)), |
There was a problem hiding this comment.
p should be explicit in takeWhile_append_dropWhile since that's a rewriting lemma
| · rw [List.count_tail l 1 hlnil, hl₀, hlast, beq_self_eq_true, if_pos rfl, Nat.add_sub_cancel] | ||
| · rw [List.count_tail l (-1) hlnil, hl₁, hlast, if_neg (by decide), Nat.sub_zero] | ||
| · rw [List.count_tail hlnil, hl₀, hlast, beq_self_eq_true, if_pos rfl, Nat.add_sub_cancel] | ||
| · rw [List.count_tail hlnil, hl₁, hlast, if_neg (by decide), Nat.sub_zero] |
There was a problem hiding this comment.
l now being implicit in count_tail is great, but is a kept explicit as the last argument? ie is it count_tail {l : List α} {a : α} (h : l ≠ []) or count_tail {l : List α} (h : l ≠ []) (a : α). It should be the latter
| simp | ||
| · have A : (ofFn f).take i = (ofFn f).take i.succ := by | ||
| rw [← length_ofFn f] at h | ||
| rw [← length_ofFn (f := f)] at h |
There was a problem hiding this comment.
f should be explicit in length_ofFn since it's a rewriting lemma
| (l.map f).prod = f l.prod := by | ||
| simp only [prod, foldr_map, ← map_one f] | ||
| exact l.foldr_hom f (· * ·) (f · * ·) 1 (fun x y => (map_mul f x y).symm) | ||
| exact l.foldr_hom f (fun x y => (map_mul f x y).symm) |
There was a problem hiding this comment.
Don't hugely mind either way here since g₁ and g₂ can technically be inferred from H : ∀ (x : α) (y : β₁), g₂ x (f y) = f (g₁ x y) but in practice won't due to higher order unification problems
| (pure_bind := fun _ _ => List.append_nil _) | ||
| (bind_assoc := List.flatMap_assoc) | ||
| (bind_pure_comp := fun _ _ => (map_eq_flatMap _ _).symm) | ||
| (bind_assoc := fun _ _ _ => List.flatMap_assoc) |
There was a problem hiding this comment.
All those arguments should stay explicit in flatMap_assoc since it's a rewriting lemma
| (bind_assoc := List.flatMap_assoc) | ||
| (bind_pure_comp := fun _ _ => (map_eq_flatMap _ _).symm) | ||
| (bind_assoc := fun _ _ _ => List.flatMap_assoc) | ||
| (bind_pure_comp := fun _ _ => map_eq_flatMap.symm) |
There was a problem hiding this comment.
All those arguments should stay explicit in map_eq_flatMap since it's a rewriting lemma
No description provided.