Repository navigation
Conversation
github-actions
Bot
added
the
tech debt
PR summary 2597daab16Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type (strong) |
|---|---|---|
| 486 | -3 | backward.privateInPublic |
| 196 | -2 | backward.privateInPublic.warn |
| 385 | -1 | adaptation notes |
Decrease in weak tech debt: (relative, absolute) = (8.00, 0.00)
| Current number | Change | Type (weak) |
|---|---|---|
| 5095 | -8 | exposed public sections |
Current commit 2597daab16
Reference commit d88814353f
This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py 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).
grunweg
left a comment
grunweg
left a comment
There was a problem hiding this comment.
Thanks for doing this! I've reviewed the first quarter of the PR so far, and have one and a half questions.
| theorem mkAlgHom_surjective (s : A → A → Prop) : Function.Surjective (mkAlgHom S s) := by | ||
| suffices Function.Surjective fun x ↦ (⟨.mk (Rel s) x⟩ : RingQuot s) by | ||
| simpa [mkAlgHom_def, mkRingHom_def] | ||
| change Function.Surjective fun x ↦ (⟨.mk (Rel s) x⟩ : RingQuot s) |
There was a problem hiding this comment.
Can you comment on this change (no pun intended)? change is usually a bit of a code smell.
There was a problem hiding this comment.
I found that the simpa proof could be replaced by rfl, and then suffices ... by rfl is equivalent to change ....
| simp only [preLiftAlgHom_def, mkAlgHom_def, mkRingHom_def, | ||
| AlgHom.coe_comp, AlgHom.coe_mk, RingHom.coe_mk, | ||
| MonoidHom.coe_mk, OneHom.coe_mk, Function.comp_apply] } | ||
| left_inv := fun f ↦ by rfl |
There was a problem hiding this comment.
Can you say a word why this is fine? You're rewriting by _def lemmas, sure (no questions), but you also have the coercion composition lemmas. I worry about us creating heavy rfl's here... can you convince me otherwise?
There was a problem hiding this comment.
I think all of the lemmas in the simp only are basic coercion/application lemmas that are fine to unfold via rfl.
grunweg
added
the
awaiting-author
grunweg
left a comment
grunweg
left a comment
There was a problem hiding this comment.
Done reviewing except for two files: just a few more comments.
|
|
||
| -/ | ||
|
|
||
| @[expose] public section |
There was a problem hiding this comment.
There's a meta def below... but I presume un-exposing that is fine.
|
(I'll be happy to review further once this passes CI; I understand there's some more work needed here.) |
grunweg
added
the
awaiting-CI
|
!radar |
|
Benchmark results for 5a9dfe3 against ca99799 are in. There are significant results. @JovanGerb Warning These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.
Large changes (1✅, 1🟥)
Medium changes (4✅, 3🟥)
Small changes (94✅, 9🟥)
|
github-actions
Bot
removed
the
awaiting-CI
|
!radar |
|
Benchmark results for 131fd44 against d888143 are in. There are significant results. @JovanGerb
Large changes (1✅, 1🟥)
Medium changes (5✅, 2🟥)
Small changes (65✅, 9🟥)
|
|
Diff to this point looks good: is there anything else to do for this PR, or shall I bors it? |
…b/mathlib4 into Jovan-irreducible_def-no_expose
|
Yes, I think it is ready now. There may be downstream uses that rely on some of these definitions where I haven't added a corresponding public |
grunweg
left a comment
grunweg
left a comment
There was a problem hiding this comment.
Can you elaborate a bit more on this:
There may be downstream uses that rely on some of these definitions
How can downstream users break? Thanks!
|
When using |
|
I see. Can you add one sentence about this to the PR description, how this is theoretically a breaking change (and how to mitigate it)? That would be excellent. |
|
With the above addressed, I think this is good to go and worthwhile clean-up. I'll wait for 24 hours in case another maintainer (or reviewer) feels strongly about further details; if not, I'll merge then. |
|
🚀 Pull request has been placed on the maintainer queue by grunweg. |
mathlib-triage
Bot
added
the
maintainer-merge
The
no_exposeattribute can be used in place ofirreducible_def, and leads to easier proofs because the definition can be unfolded the file containing the definition.Another difference is that by using
no_expose, the definition value is not exported at all, so in downstream modules it cannot be unfolded with e.g.rw [foo]orrw [foo_def]. Instead, a public lemma likefoo_defneeds to be added explicitly. This PR does that where necessary. If there is no such lemma, but you still need access to the definition value,import allcan be used as a workaround.Since mathlib now enforces downstream users to use the
modulesystem, we don't need to worry about downstream users that don't see the effects ofno_expose.