Conversation
erdOne
commented
Jun 10, 2025
|
!bench |
PR summary 4a11bc26dbImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type |
|---|---|---|
| 121 | -1 | adaptation notes |
Current commit 2f2c783e49
Reference commit 4a11bc26db
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).
|
Here are the benchmark results for commit dfd0bdc. |
|
!bench |
|
Here are the benchmark results for commit 0f49e19. Benchmark Metric Change
==================================================================
+ ~Mathlib.Algebra.Module.FinitePresentation instructions -6.8%
- ~Mathlib.AlgebraicGeometry.AffineSpace instructions 69.6%
- ~Mathlib.RingTheory.RingHom.Locally instructions 12.2% |
2 files, Instructions +8.0⬝10⁹
2 files, Instructions +7.0⬝10⁹
2 files, Instructions +6.0⬝10⁹
5 files, Instructions +5.0⬝10⁹
5 files, Instructions +3.0⬝10⁹
5 files, Instructions +2.0⬝10⁹
19 files, Instructions +1.0⬝10⁹
|
|
I think this slowdown is acceptable considering this is the right thing to do. |
kckennylau
left a comment
There was a problem hiding this comment.
I feel like changing those defs into abbrevs... is there no other way?
| /-- The canonical map sending `(m, s) ↦ m/s` -/ | ||
| def mk (m : M) (s : S) : LocalizedModule S M := | ||
| Quotient.mk' ⟨m, s⟩ | ||
| abbrev mk (m : M) (s : S) : LocalizedModule S M := m /ₒ s |
There was a problem hiding this comment.
Is m /ₒ s or mk m s the canonical form now?
There was a problem hiding this comment.
This is an intermediate step. The long term plan is to remove mk.
There was a problem hiding this comment.
Can you add that as a Todo on the docstring?
|
The whole point of this PR is to make |
|
This pull request has conflicts, please merge |
|
This pull request has conflicts, please merge |
|
Can this PR get a description explaining what it does, and why it's the correct thing to do? |
| @@ -49,6 +50,19 @@ for some (u : S), u * (s2 • m1 - s1 • m2) = 0 -/ | |||
| def r (a b : M × S) : Prop := | |||
There was a problem hiding this comment.
I get this isn't part of the PR, but I'm really not a fan of single letter defs (let alone unprotected ones!)
| -/ | ||
| def _root_.LocalizedModule : Type max u v := | ||
| Quotient (r.setoid S M) | ||
| abbrev _root_.LocalizedModule : Type max u v := |
There was a problem hiding this comment.
I imagine the end-goal here is to deprecate LocalizedModule in favor of OreLocalization, am I right? If so, can you add that to the module docstring as a ## Todo? (And if not, can you explain the design you're going for an ## Implementation notes?)
| /-- The canonical map sending `(m, s) ↦ m/s` -/ | ||
| def mk (m : M) (s : S) : LocalizedModule S M := | ||
| Quotient.mk' ⟨m, s⟩ | ||
| abbrev mk (m : M) (s : S) : LocalizedModule S M := m /ₒ s |
There was a problem hiding this comment.
Can you add that as a Todo on the docstring?
| simp only [smul_add, ← mul_smul, mul_comm, | ||
| mul_left_comm] at hu1' hu2' ⊢ | ||
| rw [hu1', hu2']⟩ | ||
| theorem zero_mk (s : S) : mk (0 : M) s = 0 := by simp [mk] |
There was a problem hiding this comment.
Why is this no longer simp?
| theorem zero_mk (s : S) : mk (0 : M) s = 0 := | ||
| mk_eq.mpr ⟨1, by rw [one_smul, smul_zero, smul_zero, one_smul]⟩ | ||
|
|
||
| instance : Add (LocalizedModule S M) where |
There was a problem hiding this comment.
(Just to be clear, this instance is now automatically inferred, right?)
This is part of Hahn embedding theorem leanprover-community#27268, where an a ordered group is first embedded in a divisible group / Q-module. I am aware at leanprover-community#25662 there is also an ongoing rewrite of `LocalizedModule` that this PR uses. Hopefully I avoided interfering it by using mostly with public API.
This is part of Hahn embedding theorem leanprover-community#27268, where an a ordered group is first embedded in a divisible group / Q-module. I am aware at leanprover-community#25662 there is also an ongoing rewrite of `LocalizedModule` that this PR uses. Hopefully I avoided interfering it by using mostly with public API.
|
superseded by #31862 |