[Merged by Bors] - chore: adaptations for nightly-2024-11-20

[kim-em]

No description provided.

[github-actions]

PR summary 66995538bc

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Data.Vector.Mem	396	394	-2 (-0.51%)
Mathlib.Data.List.Sym	467	465	-2 (-0.43%)
Mathlib.Combinatorics.Enumerative.Composition	600	598	-2 (-0.33%)
Mathlib.Testing.Plausible.Functions	677	675	-2 (-0.30%)
Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue	698	696	-2 (-0.29%)
Mathlib.Data.List.NodupEquivFin	363	362	-1 (-0.28%)
Mathlib.Data.Finset.Sort	484	483	-1 (-0.21%)
Mathlib.Data.List.Cycle	484	483	-1 (-0.21%)
Mathlib.Analysis.Calculus.FDeriv.Mul	1506	1505	-1 (-0.07%)
Mathlib.Analysis.FunctionalSpaces.SobolevInequality	2086	2085	-1 (-0.05%)

Import changes for all files

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

---

Declarations diff

+ getLast_filter'
+ getMorphismTheorems
+ getTransitionTheorems
+ subset_of_le
+ zero
- 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
- 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.43, 0.54)

Current number	Change	Type
5077	-11	porting notes
203	18	adaptation notes
225	4	disabled simpNF lints
1556	-2	erw
16	7	maxHeartBeats modifications

Current commit 66995538bc
Reference commit 232f84f526

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).

[eric-wieser]

Does eraseIdx! panic?

[eric-wieser]

Which is to say; I think this might have been relying on the old behavior that eraseIdx was a no-op if the index was out of bounds.

[kim-em]

Okay, I'll change this to eraseIdxIfInBounds. It would be lovely if we could have a test demonstrating that it is relying on this, I guess. @adomani, do you know if what this should do?

[adomani]

I am late for this party!

Anyway, preWS is always (I hope!) an array with at least 2 entries: split is obtained via String.split on some string and therefore always consists of at least one entry. Next, preWS loops over the entries of split appending two natural numbers on every loop. The result is preWS that looks like

#[0, <an odd number of remaining entries>]

So, whether or not you use a function that panics there, I think that the resulting code will not panic.

[kim-em]

bors merge

[mathlib-bors]

Pull request successfully merged into bump/v4.15.0.

Build succeeded:

• Lint style
• Build