[Merged by Bors] - feat(Combinatorics/SimpleGraph/Walk): add `dropLast` by Command-Master · Pull Request #16382 · leanprover-community/mathlib4

Command-Master · 2024-09-01T07:01:21Z

depends on: [Merged by Bors] - chore(Combinatorics/SimpleGraph): remove sndOfNotNil #16352
depends on: [Merged by Bors] - feat(Combinatorics/SimpleGraph/Walk): add penultimate and snd #16769

github-actions · 2024-09-01T07:02:05Z

PR summary 2647207846

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ concat_dropLast
+ dropLast
+ dropLast_concat
+ dropLast_cons_cons
+ dropLast_cons_nil
+ dropLast_cons_of_not_nil
+ dropLast_nil
+ getVert_mem_support
+ nil_reverse
+ penultimate_nil
+ take

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.

No changes to technical debt.

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

pimotte · 2024-09-08T06:23:43Z

I don't think I really have quite enough experience to do a full-on review, but I do have a suggestion:

Either reintroduce snd/second (without the notNil), or use p.getVert (p.length - 1) directly to keep the whole thing consistent. I'm tempted to advise the latter, given the direction my PR was taking, but maybe @YaelDillies can weigh in on this?:)

YaelDillies

Yes indeed I would tend to agree that we don't want penultimate/dropLast for the same reason we got rid of sndOfNeNil.

There is an argument to be made that p appears twice in the body of penultimate/dropLast though...

Command-Master · 2024-09-08T12:54:00Z

dropLast mirrors tail, so I don't see a reason to drop it. Regarding penultimate, I also think it's good, mainly due to p appearing twice in the definition.

YaelDillies · 2024-09-08T12:56:32Z

I would then suggest you reintroduce sndOfNeNil under the name snd (and without the ¬ Nil assumption), for symmetry. Maybe make this PR be about dropLast (which is uncontentious as it mirrors tail) and move penultimate to a second PR depending on this one?

Command-Master · 2024-09-10T07:50:50Z

But I need penultimate for dropLast

YaelDillies · 2024-09-11T10:37:59Z

Then can you make penultimate and snd a preliminary PR to dropLast?

Mathlib/Combinatorics/SimpleGraph/Walk.lean

YaelDillies

Thanks!

maintainer delegate

Mathlib/Combinatorics/SimpleGraph/Walk.lean

github-actions · 2025-01-06T21:35:05Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Command-Master · 2025-01-08T05:48:49Z

Do I need to do maintainer merge? How does maintainer delegate work?

YaelDillies · 2025-01-08T09:19:37Z

Works the same as maintainer merge, but telling maintainers to delegate

b-mehta · 2025-01-20T19:55:38Z

It looks like this one doesn't add penultimate any more, right?

sgouezel · 2025-01-23T18:19:43Z

bors d+
Can you fix the PR title before merging?

mathlib-bors · 2025-01-23T18:19:46Z

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

YaelDillies · 2025-02-11T11:43:43Z

Since the name was so trivial to fix, I did it myself.

maintainer merge

github-actions · 2025-02-11T11:44:03Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

b-mehta · 2025-02-11T20:22:53Z

Thanks!

bors merge

Co-authored-by: Daniel Weber <55664973+Command-Master@users.noreply.github.com>

mathlib-bors · 2025-02-11T21:00:07Z

Pull request successfully merged into master.

Build succeeded:

Command-Master added RFC Request for comment t-combinatorics Combinatorics labels Sep 1, 2024

Command-Master mentioned this pull request Sep 1, 2024

[Merged by Bors] - chore(Combinatorics/SimpleGraph): remove sndOfNotNil #16352

Closed

Command-Master added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Sep 1, 2024

ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Sep 1, 2024

Command-Master added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Sep 1, 2024

ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Sep 4, 2024

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 4, 2024

Update

3f47258

Command-Master force-pushed the CM_wsnd branch from 84cfca6 to 3f47258 Compare September 6, 2024 03:26

Command-Master changed the title ~~refactor(Combinatorics/SimpleGraph/Walk): change sndOfNotNil and tail to not require a not-nil assumption, and add penultimate and dropLast~~ refactor(Combinatorics/SimpleGraph/Walk): add penultimate and dropLast Sep 6, 2024

Command-Master removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) RFC Request for comment labels Sep 6, 2024

Command-Master added 2 commits September 6, 2024 06:34

Fix

a36e839

Fix

cacdb4a

Command-Master changed the title ~~refactor(Combinatorics/SimpleGraph/Walk): add penultimate and dropLast~~ feat(Combinatorics/SimpleGraph/Walk): add penultimate and dropLast Sep 6, 2024

Command-Master added the RFC Request for comment label Sep 6, 2024

Command-Master requested a review from pimotte September 7, 2024 02:59

Command-Master requested a review from YaelDillies September 8, 2024 08:51

YaelDillies reviewed Sep 8, 2024

View reviewed changes

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Sep 13, 2024

Command-Master removed the RFC Request for comment label Sep 14, 2024

Command-Master mentioned this pull request Nov 29, 2024

[Merged by Bors] - feat(Combinatorics/SimpleGraph/Walk): add penultimate and snd #16769

Closed

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 16, 2024

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 6, 2025

YaelDillies reviewed Jan 6, 2025

View reviewed changes

Mathlib/Combinatorics/SimpleGraph/Walk.lean Outdated Show resolved Hide resolved

Mathlib/Combinatorics/SimpleGraph/Walk.lean Outdated Show resolved Hide resolved

Mathlib/Combinatorics/SimpleGraph/Walk.lean Outdated Show resolved Hide resolved

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 6, 2025

Apply suggestions from code review

506503c

Command-Master removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 6, 2025

Command-Master added 3 commits January 6, 2025 22:34

Fix

375ad87

Fix name

093ac20

Minimize diff

0589003

YaelDillies approved these changes Jan 6, 2025

View reviewed changes

Mathlib/Combinatorics/SimpleGraph/Walk.lean Outdated Show resolved Hide resolved

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 6, 2025

Update Mathlib/Combinatorics/SimpleGraph/Walk.lean

2647207

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jan 23, 2025

YaelDillies changed the title ~~feat(Combinatorics/SimpleGraph/Walk): add penultimate and dropLast~~ feat(Combinatorics/SimpleGraph/Walk): add dropLast Feb 11, 2025

ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Feb 11, 2025

mathlib-bors bot pushed a commit that referenced this pull request Feb 11, 2025

feat(Combinatorics/SimpleGraph/Walk): add dropLast (#16382)

acfac8d

Co-authored-by: Daniel Weber <55664973+Command-Master@users.noreply.github.com>

mathlib-bors bot changed the title ~~feat(Combinatorics/SimpleGraph/Walk): add dropLast~~ [Merged by Bors] - feat(Combinatorics/SimpleGraph/Walk): add dropLast Feb 11, 2025

mathlib-bors bot closed this Feb 11, 2025

mathlib-bors bot deleted the CM_wsnd branch February 11, 2025 21:00

SnirBroshi mentioned this pull request Nov 23, 2025

[Merged by Bors] - feat(Combinatorics/SimpleGraph): split Walk.lean into 5 files #31573

Closed

Conversation

Command-Master commented Sep 1, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Sep 1, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 2647207846

Import changes for modified files

Declarations diff

Uh oh!

pimotte commented Sep 8, 2024

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Command-Master commented Sep 8, 2024

Uh oh!

YaelDillies commented Sep 8, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Command-Master commented Sep 10, 2024

Uh oh!

YaelDillies commented Sep 11, 2024

Uh oh!

Uh oh!

Uh oh!

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

github-actions bot commented Jan 6, 2025

Uh oh!

Command-Master commented Jan 8, 2025

Uh oh!

YaelDillies commented Jan 8, 2025

Uh oh!

b-mehta commented Jan 20, 2025

Uh oh!

sgouezel commented Jan 23, 2025

Uh oh!

mathlib-bors bot commented Jan 23, 2025

Uh oh!

YaelDillies commented Feb 11, 2025

Uh oh!

github-actions bot commented Feb 11, 2025

Uh oh!

b-mehta commented Feb 11, 2025

Uh oh!

mathlib-bors bot commented Feb 11, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

Command-Master commented Sep 1, 2024 •

edited

Loading

github-actions bot commented Sep 1, 2024 •

edited

Loading

YaelDillies commented Sep 8, 2024 •

edited

Loading