chore: adaptations for nightly-2025-02-20#22144
Merged
kim-em merged 4889 commits intobump/v4.18.0from Feb 21, 2025
Merged
Conversation
PR summary 9c2579601bImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type |
|---|---|---|
| 111 | 5 | adaptation notes |
| 7 | 5 | maxHeartBeats modifications |
Current commit 9c2579601b
Reference commit 5308324503
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).
kbuzzard
reviewed
Feb 20, 2025
| @@ -44,12 +52,4 @@ theorem extract_eq_of_size_le_end {l p : Nat} {a : Array α} (h : a.size ≤ l) | |||
| a.extract p l = a.extract p a.size := by | |||
| simp only [extract, Nat.min_eq_right h, Nat.sub_eq, mkEmpty_eq, Nat.min_self] | |||
|
|
|||
| theorem extract_extract {s1 e2 e1 s2 : Nat} {a : Array α} (h : s1 + e2 ≤ e1) : | |||
Member
There was a problem hiding this comment.
Did this get upstreamed or just forgotten about?
kbuzzard
approved these changes
Feb 20, 2025
Member
kbuzzard
left a comment
There was a problem hiding this comment.
I can't guess why the changes to lake-manifest.json involve changing main or master to nightly-testing sometimes, somehow I guess I'm confused about why these nightly branches need to make such changes. But I'm trusting that things are OK here. The only other thing I didn't understand was the addition of the set_option linter.deprecated false in lines in Mathlib/Data/List/Iterate.lean and Mathlib/Data/List/Nodup.lean. If these are as expected then this looks good to go to me. At some point we should flag that mathlib seems to be very inconsistent with indentation in multiline class definitions but that is definitely not an issue for this PR!
bors d+
Contributor
|
✌️ kim-em can now approve this pull request. To approve and merge a pull request, simply reply with |
kim-em
added a commit
that referenced
this pull request
Mar 10, 2025
* chore: adaptations for nightly-2025-02-20 * Merge master into nightly-testing * minor reverts * more * deprecation * another * more * restore check-yaml * . * . * chore: adaptations for nightly-2025-02-20 (#22144) * lake update * fixes * fix namespace * fix test * Merge master into nightly-testing * chore: bump to nightly-2025-02-06 * copy test from master * Merge master into nightly-testing * chore: bump to nightly-2025-02-07 * chore: bump to nightly-2025-02-08 * update * chore: bump to nightly-2025-02-09 * didn't commit * fix * fix test * Update lean-toolchain for testing leanprover/lean4#7013 * chore: bump to nightly-2025-02-10 * fixes for leanprover/lean4#7013 * fixes for leanprover/lean4#7013 * Trigger CI for leanprover/lean4#7013 * chore: bump to nightly-2025-02-11 * update * Update lean-toolchain for testing leanprover/lean4#7046 * Trigger CI for leanprover/lean4#7046 * Switch from mk to ofBitVec * chore: bump to nightly-2025-02-12 * Update lean-toolchain for testing leanprover/lean4#7050 * lake update * lake update * fixes * another maxheartbeats * fix tests * Update lean-toolchain for testing leanprover/lean4#7059 * fix * chore: bump to nightly-2025-02-13 * lake update * fixes * lake exe shake --fix * Update lean-toolchain for testing leanprover/lean4#7069 * Trigger CI for leanprover/lean4#7069 * chore: adaptations for nightly-2025-02-13 * remove upstreamed * Trigger CI for leanprover/lean4#7059 * Trigger CI for leanprover/lean4#7059 * chore: bump to nightly-2025-02-14 * Trigger CI for leanprover/lean4#7069 * Trigger CI for leanprover/lean4#7069 * Update lean-toolchain for testing leanprover/lean4#7082 * quite a bit more to go * lake update * fix merge * fix * adapt * adapt * Trigger CI for leanprover/lean4#7082 * Trigger CI for leanprover/lean4#7069 * lake update * lake update * fixes * fixes * chore: bump to nightly-2025-02-15 * Trigger CI for leanprover/lean4#7069 * Update lean-toolchain for testing leanprover/lean4#7100 * chore: bump to nightly-2025-02-16 * fixes * fixes 2 * fixes 3 * built mathlib * Trigger CI for leanprover/lean4#7069 * fix simps test * fixes for leanprover/lean4#7059 * fix: cache lib dir (adaption for lean4#7001) (#21967) * fixes * fixes for leanprover/lean4#7059 * restore broken files * chore: bump to nightly-2025-02-17 * lake update * lake update * oops * comment out broken files * longFile * oops, one more * . * searchPath * . * Update lean-toolchain for testing leanprover/lean4#7103 * fixes * update manifest * fix * fix * Trigger CI for leanprover/lean4#7103 * chore: bump to nightly-2025-02-18 * lake update * deprecations * restore computability files broken by defeq yesterday * fixes * chore: adaptations for nightly-2025-02-18 * chore: bump to nightly-2025-02-19 * lake update * fixes * fix merge * chore: adaptations for nightly-2025-02-19 * Merge master into nightly-testing * chore: bump to nightly-2025-02-20 * fix merge * chore: adaptations for nightly-2025-02-20 * minor reverts * more * deprecation * another * more * restore check-yaml * . * . --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Markus Himmel <markus@lean-fro.org> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Mac Malone <mac@lean-fro.org> * chore: bump to nightly-2025-02-21 * chore: bump to nightly-2025-02-22 * chore(Tactic/DeriveTraversable): adapt to `auxDeclToFullName` relocation * Update lean-toolchain for testing leanprover/lean4#7196 * fixes * update batteries * update proofwidgets * Trigger CI for leanprover/lean4#7166 * Trigger CI for leanprover/lean4#7166 * chore: bump to nightly-2025-02-24 * lake update * fixes * deprecations * . * archive * fix tests * fix tests * chore: adaptations for nightly-2025-02-24 (#22266) Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com> * chore: bump to nightly-2025-02-25 * Trigger CI for leanprover/lean4#7166 * Trigger CI for leanprover/lean4#7166 * Trigger CI for leanprover/lean4#7166 * Trigger CI for leanprover/lean4#7166 * Adapt * Trigger CI for leanprover/lean4#7166 * revert Mathlib/Data/Multiset/Basic, and refix * Merge master into nightly-testing * chore: bump to nightly-2025-02-26 * remove upstreamed * fix * fix tests * Apply suggestions from code review Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk> * chore: adaptations for nightly-2025-02-26 (#22347) Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> * chore: bump to nightly-2025-02-27 * Trigger CI for leanprover/lean4#7166 * Update lean-toolchain for testing leanprover/lean4#7259 * fix * I would not have guessed that this lemma already exists! * chore: bump to nightly-2025-02-28 * fix * chore: bump to nightly-2025-03-01 * chore: bump to nightly-2025-03-02 * Merge master into nightly-testing * deprecation * Trigger CI for leanprover/lean4#7166 * deprecation * chore: adaptations for nightly-2025-03-02 (#22460) Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Markus Himmel <markus@lean-fro.org> * chore: adaptations for nightly-2025-03-02 * chore: bump to nightly-2025-03-03 * remove upstreamed * chore: adaptations for nightly-2025-03-03 * Trigger CI for leanprover/lean4#7166 * chore: adaptations for nightly-2025-03-03 (#22493) Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net> * bump toolchain and dependencies * Trigger CI for leanprover/lean4#7166 * chore: bump to nightly-2025-03-04 * lake update * Trigger CI for leanprover/lean4#7166 * chore: bump to nightly-2025-03-05 * fix? * add adaptation notes to revert _root_ * Update lean-toolchain for testing leanprover/lean4#7358 * chore: bump to nightly-2025-03-06 * chore: adaptations for nightly-2025-03-06 * chore: adaptations for nightly-2025-03-06 * Merge master into nightly-testing * chore: bump to nightly-2025-03-06 * Update lean-toolchain for testing leanprover/lean4#7261 * fixes for leanprover/lean4#7358 * fixes for leanprover/lean4#7358 * fixes for leanprover/lean4#7358 * Trigger CI for leanprover/lean4#7358 * Trigger CI for leanprover/lean4#7261 * fix Mathlib.Linter.getNamesFrom * chore: adaptations for nightly-2025-03-06 * chore: bump to nightly-2025-03-07 * lake update * add_div is protected * Update lean-toolchain for testing leanprover/lean4#7378 * More like that * adapt * Trigger CI for leanprover/lean4#7378 * Fix * fix * chore: bump to nightly-2025-03-08 * lake update * chore: bump to nightly-2025-03-09 * chore(RingTheory/LocalRing/ResidueField/Ideal): increase `simp` prio, analogous to #22215 * process adaptation notes --------- Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Markus Himmel <markus@lean-fro.org> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Mac Malone <mac@lean-fro.org> Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com> Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Matthew Ballard <matt@mrb.email> Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
7 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.