review: just the basics

[thorimur]

This ultra-quick review of #35750 doesn't check for good behavior or maintainable code; instead, as per the zulip thread, it merely

• adds disclaimers
• makes some things private
• reviews documentation and behavior in the public module
• makes sure that nothing catastrophic is happening

---

[github-actions]

PR summary d300915bf1

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
There are 6696 files with changed transitive imports taking up over 297229 characters: this is too many to display!
You can run scripts/import_trans_difference.sh all locally to see the whole output.

---

Declarations diff

+ A
+ B
+ Gr'
+ MyAction
+ MyPred
+ MySub₂
+ MySub₂.toAddSubgroup
+ Num'
+ Sm'
+ TraceResult
+ VisitStep
+ Zo'
+ analyzeTraces
+ b
+ dedupByString
+ extractInstName
+ instance : Gr' Int
+ instance : Membership ℕ (MyPred ℕ) where mem s a := s a
+ instance : Singleton ℕ (MyPred ℕ) where singleton a x := x = a
+ instance : Zo' Int
+ instance {G : Type} [AddCommGroup G] : CoeSort (MySub₂ G) Type
+ instance {n} : Num' Int n
+ instance {α} [Zo' α] : Num' α 0
+ instance {α} [h : Gr' α] : Sm' α := { h with }
+ myOp
+ myPredBoundedOrder
+ myPredCompleteLattice
+ myPredDistribLattice
+ myPred_disjoint_singleton_right
+ mySub₂AddCommGroup
+ mySub₂AddCommMonoid
+ mySub₂MyAction
+ myTestFun
+ onlyOnDefEqNodes
+ reportDefEqAbuse
+ stripTraceResultPrefix
+ testCoersion
+ testVirtualParent
+ testVirtualParentFixed
+ test_zo_cmd_abuse
+ traceResultOf
+ visitWithAndAscendM
+ visitWithM
+ zo_eq_iff
++ instance {V : Type} [AddCommGroup V] [Module ℝ V] {l : Submodule ℝ V} :

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 scripts/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
11957	1	backward.isDefEq

Current commit 7decaf34c0
Reference commit d300915bf1

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[Vierkantor]

bors d+

[mathlib-bors]

✌️ thorimur can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[thorimur]

Hmm, I'm a little worried about using bors to merge into a non-master branch? Will it know to merge it correctly?

Just in case I don't find out I'll wait for @kim-em to merge this into the base branch by default :)

[bryangingechen]

bors should work for merging into non master branches. I think the only slightly odd thing is that bors only has one queue overall, not separate queues for separate branches, so this would wait in line with the other batches on the queue that will get merged into master.