chore: adaptations for nightly-2024-11-25#19494
Conversation
…hlib4 into nightly-testing
…hlib4 into nightly-testing
PR summary d028e6b0ab
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.SetTheory.Cardinal.Basic | 640 | 636 | -4 (-0.62%) |
| Mathlib.Data.Num.Bitwise | 401 | 399 | -2 (-0.50%) |
| Mathlib.Logic.Small.List | 401 | 399 | -2 (-0.50%) |
| Mathlib.Data.Sym.Basic | 435 | 433 | -2 (-0.46%) |
| Mathlib.Data.Sym.Sym2 | 467 | 465 | -2 (-0.43%) |
| Mathlib.Data.Fintype.Vector | 475 | 473 | -2 (-0.42%) |
| Mathlib.Computability.TuringMachine | 483 | 481 | -2 (-0.41%) |
| Mathlib.Logic.Equiv.List | 497 | 495 | -2 (-0.40%) |
| Mathlib.Data.Fintype.Fin | 501 | 499 | -2 (-0.40%) |
| Mathlib.Data.Fintype.BigOperators | 521 | 519 | -2 (-0.38%) |
| Mathlib.Computability.Primrec | 556 | 554 | -2 (-0.36%) |
| Mathlib.Computability.Partrec | 561 | 559 | -2 (-0.36%) |
| Mathlib.Computability.Halting | 563 | 561 | -2 (-0.36%) |
| Mathlib.Computability.TMToPartrec | 602 | 600 | -2 (-0.33%) |
| Mathlib.Topology.List | 763 | 761 | -2 (-0.26%) |
| Mathlib.LinearAlgebra.Prod | 766 | 764 | -2 (-0.26%) |
| Mathlib.GroupTheory.Perm.Cycle.Type | 895 | 894 | -1 (-0.11%) |
| Mathlib.Algebra.Module.FreeLocus | 1790 | 1789 | -1 (-0.06%) |
Import changes for all files
| Files | Import difference |
|---|---|
| There are 3683 files with changed transitive imports taking up over 159485 characters: this is too many to display! | |
You can run scripts/import_trans_difference.sh all locally to see the whole output. |
Declarations diff
+ Mathlib.Vector.Perm.isSetoid
+ Mathlib.Vector.countable
+ Mathlib.Vector.encodable
+ getLast_filter'
+ getMorphismTheorems
+ getTransitionTheorems
+ instance (n : ℕ) : TopologicalSpace (Mathlib.Vector α n) := by unfold Mathlib.Vector; infer_instance
+ instance : Coe (Mathlib.Vector α n) (Sym α n) where coe x := ofVector x
+ subset_of_le
+ zero
++-- GlueData
++-- Vec
++-- of_eq
+-+- vector_cons
+-+- vector_get
+-+- vector_head
+-+- vector_length
+-+- vector_ofFn'
+-+- vector_tail
+-+- vector_toList
- Vector.Perm.isSetoid
- eraseIdx_insertIdx
- find?_eq_some_iff_getElem
- getElem_insertIdx_of_lt
- getElem_insertIdx_self
- getLast_filter
- getLast_ofFn
- head_ofFn
- insertIdx_comm
- insertIdx_eraseIdx_of_ge
- insertIdx_eraseIdx_of_le
- insertIdx_length_self
- insertIdx_of_length_lt
- insertIdx_succ_cons
- insertIdx_succ_nil
- insertIdx_zero
- instance (n : ℕ) : TopologicalSpace (Vector α n) := by unfold Vector; infer_instance
- instance : Coe (Vector α n) (Sym α n) where coe x := ofVector x
- instance _root_.Vector.countable [Countable α] {n} : Countable (Vector α n)
- instance _root_.Vector.encodable [Encodable α] {n} : Encodable (Vector α n)
- length_insertIdx
- length_insertIdx_le_succ
- length_le_length_insertIdx
- mapIdxGo_append
- mem_insertIdx
- modifyNthTail_modifyNthTail
- modifyTailIdx_modifyTailIdx
- modifyTailIdx_modifyTailIdx_le
- modifyTailIdx_modifyTailIdx_same
- ofFn_eq_nil_iff
- ofFn_succ
- ofFn_zero
--- discrTreeConfig
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) = (7.41, 0.54)
| Current number | Change | Type |
|---|---|---|
| 5024 | -11 | porting notes |
| 202 | 18 | adaptation notes |
| 204 | 4 | disabled simpNF lints |
| 1550 | -2 | erw |
| 16 | 7 | maxHeartBeats modifications |
Current commit d028e6b0ab
Reference commit 6e1b417164
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).
No description provided.