chore: adaptations for nightly-2025-01-02#20402
Conversation
PR summary 816051e806
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Tactic.DeriveToExpr | 21 | 0 | -21 (-100.00%) |
| Mathlib.Tactic.ToExpr | 23 | 19 | -4 (-17.39%) |
| Mathlib.Tactic.ITauto | 46 | 43 | -3 (-6.52%) |
| Mathlib.Algebra.BigOperators.Group.List | 391 | 386 | -5 (-1.28%) |
| Mathlib.Tactic.Common | 237 | 234 | -3 (-1.27%) |
| Mathlib.Data.List.Lex | 287 | 284 | -3 (-1.05%) |
| Mathlib.Data.List.Chain | 290 | 287 | -3 (-1.03%) |
| Mathlib.Combinatorics.Enumerative.DoubleCounting | 599 | 594 | -5 (-0.83%) |
| Mathlib.ModelTheory.Semantics | 655 | 650 | -5 (-0.76%) |
| Mathlib.LinearAlgebra.LinearIndependent | 886 | 881 | -5 (-0.56%) |
| Mathlib.RingTheory.Kaehler.JacobiZariski | 1392 | 1389 | -3 (-0.22%) |
| Mathlib.Tactic | 2447 | 2444 | -3 (-0.12%) |
Import changes for all files
| Files | Import difference |
|---|---|
| There are 4926 files with changed transitive imports taking up over 208917 characters: this is too many to display! | |
You can run scripts/import_trans_difference.sh all locally to see the whole output. |
Declarations diff
+ decidableLT'
+ instance (priority := low) nat (n : ℕ) : OfNat ONote n
+ instance (priority := low) {n : ℕ} : OfNat PosNum (n + 1)
+ repr_zero
- Lex
- ToLevel.imax
- ToLevel.max
- ToLevel.{u}
- countP_flatMap
- count_flatMap
- decidableLT
- fixIndType
- getElem_cons
- instance : ToLevel.{0}
- instance [ToLevel.{u}] : ToLevel.{u+1}
- instance {n : ℕ} : OfNat PosNum (n + 1)
- instance {α : Type u} [ToExpr α] [ToLevel.{u}] : ToExpr (Array α)
- length_flatMap
- lt_div_iff_mul_lt
- mkAppNTerm
- mkAuxFunction
- mkInstanceCmds
- mkLocalInstanceLetDecls
- mkMutualBlock
- mkToExprBody
- mkToExprHeader
- mkToExprInstanceCmds
- mkToExprInstanceHandler
- mkToLevelBinders
- mkToTypeExpr
- nat
- nil_le
- nil_lt_cons
- replicate_succ'
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) = (1.00, 0.00)
| Current number | Change | Type |
|---|---|---|
| 208 | 1 | adaptation notes |
Current commit 816051e806
Reference commit e0a3be5c67
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.