Skip to content

[Merged by Bors] - chore(Combinatorics/SimpleGraph): rename Walks folder to Walk#36854

Closed
YaelDillies wants to merge 1 commit intoleanprover-community:masterfrom
YaelDillies:simple_graph_walks
Closed

[Merged by Bors] - chore(Combinatorics/SimpleGraph): rename Walks folder to Walk#36854
YaelDillies wants to merge 1 commit intoleanprover-community:masterfrom
YaelDillies:simple_graph_walks

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

It is unusual to pluralise folder names, and furthermore this folder is about the Walk type.


Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 19, 2026

PR summary 96eec06566

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Combinatorics.SimpleGraph.Walks.Counting -581
Mathlib.Combinatorics.SimpleGraph.Walks.Decomp -577
Mathlib.Combinatorics.SimpleGraph.Walks.Subwalks -576
Mathlib.Combinatorics.SimpleGraph.Walks.Maps -575
Mathlib.Combinatorics.SimpleGraph.Walks.Operations -548
Mathlib.Combinatorics.SimpleGraph.Walks.Traversal -546
Mathlib.Combinatorics.SimpleGraph.Walks.Basic -545
Mathlib.Combinatorics.SimpleGraph.Walk.Basic 545
Mathlib.Combinatorics.SimpleGraph.Walk.Traversal 546
Mathlib.Combinatorics.SimpleGraph.Walk.Operations 548
Mathlib.Combinatorics.SimpleGraph.Walk.Maps 575
Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks 576
Mathlib.Combinatorics.SimpleGraph.Walk.Decomp 577
Mathlib.Combinatorics.SimpleGraph.Walk.Counting 581

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.


No changes to technical debt.

You can run this locally as

./scripts/reporting/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).

note: file Mathlib/Combinatorics/SimpleGraph/Walks/Decomp.lean` was renamed to `Mathlib/Combinatorics/SimpleGraph/Walk/Decomp.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file Mathlib/Combinatorics/SimpleGraph/Walks/Counting.lean` was renamed to `Mathlib/Combinatorics/SimpleGraph/Walk/Counting.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file Mathlib/Combinatorics/SimpleGraph/Walks/Basic.lean` was renamed to `Mathlib/Combinatorics/SimpleGraph/Walk/Basic.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file Mathlib/Combinatorics/SimpleGraph/Walks/Subwalks.lean` was renamed to `Mathlib/Combinatorics/SimpleGraph/Walk/Subwalks.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file Mathlib/Combinatorics/SimpleGraph/Walks/Operations.lean` was renamed to `Mathlib/Combinatorics/SimpleGraph/Walk/Operations.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file Mathlib/Combinatorics/SimpleGraph/Walks/Traversal.lean` was renamed to `Mathlib/Combinatorics/SimpleGraph/Walk/Traversal.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file Mathlib/Combinatorics/SimpleGraph/Walks/Maps.lean` was renamed to `Mathlib/Combinatorics/SimpleGraph/Walk/Maps.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

@github-actions github-actions bot added file-removed A Lean module was (re)moved without a `deprecated_module` annotation t-combinatorics Combinatorics labels Mar 19, 2026
@mathlib-merge-conflicts mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 25, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

This pull request has conflicts, please merge master and resolve them.

@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 25, 2026
@mathlib-merge-conflicts mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 27, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

This pull request has conflicts, please merge master and resolve them.

@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 27, 2026
@SnirBroshi
Copy link
Copy Markdown
Collaborator

FWIW as of now 10% of the folders in mathlib end with an s (which usually implies they're pluralized, though not always)
I prefer Walks, but I'm okay with this change if the general trend is to stop pluralizing and rename those 10%.

@mathlib-merge-conflicts mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 30, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

This pull request has conflicts, please merge master and resolve them.

It is unusual to pluralise folder names, and furthermore this folder is about the `Walk` type.
@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 31, 2026
@YaelDillies
Copy link
Copy Markdown
Contributor Author

FWIW as of now 10% of the folders in mathlib end with an s (which usually implies they're pluralized, though not always) I prefer Walks, but I'm okay with this change if the general trend is to stop pluralizing and rename those 10%.

Are these folders named after a type? Here, the SimpleGraph.Walk folder is named after the SimpleGraph.Walk type, which is a good property to have

@b-mehta
Copy link
Copy Markdown
Contributor

b-mehta commented Apr 1, 2026

Thanks

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Apr 1, 2026
…6854)

It is unusual to pluralise folder names, and furthermore this folder is about the `Walk` type.
@mathlib-triage mathlib-triage bot added the ready-to-merge This PR has been sent to bors. label Apr 1, 2026
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Apr 1, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(Combinatorics/SimpleGraph): rename Walks folder to Walk [Merged by Bors] - chore(Combinatorics/SimpleGraph): rename Walks folder to Walk Apr 1, 2026
@mathlib-bors mathlib-bors bot closed this Apr 1, 2026
@SnirBroshi
Copy link
Copy Markdown
Collaborator

Should we also rename Paths.lean since it's about the type Path?
(alternatively, can we deprecate Path and just use the unbundled IsPath?)

@YaelDillies YaelDillies deleted the simple_graph_walks branch April 1, 2026 14:20
@YaelDillies
Copy link
Copy Markdown
Contributor Author

Should we also rename Paths.lean since it's about the type Path? (alternatively, can we deprecate Path and just use the unbundled IsPath?)

Sure, feel free to do so!

aditya-ramabadran pushed a commit to aditya-ramabadran/mathlib4 that referenced this pull request Apr 1, 2026
…anprover-community#36854)

It is unusual to pluralise folder names, and furthermore this folder is about the `Walk` type.
xroblot pushed a commit to xroblot/mathlib4 that referenced this pull request Apr 3, 2026
…anprover-community#36854)

It is unusual to pluralise folder names, and furthermore this folder is about the `Walk` type.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

file-removed A Lean module was (re)moved without a `deprecated_module` annotation ready-to-merge This PR has been sent to bors. t-combinatorics Combinatorics

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants