Skip to content

[Merged by Bors] - chore: rename fun_prop test files#39278

Closed
grunweg wants to merge 1 commit into
leanprover-community:masterfrom
grunweg:movefunproptest
Closed

[Merged by Bors] - chore: rename fun_prop test files#39278
grunweg wants to merge 1 commit into
leanprover-community:masterfrom
grunweg:movefunproptest

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@grunweg grunweg commented May 13, 2026

After #39261, the only remaining files are fun_prop2.lean and fun_prop_dev.lean. Rename them to something more telling, and make them UpperCamelCase while at it. (The latter is mathlib's policy for module names anyway.)

Open in Gitpod

@grunweg grunweg requested a review from lecopivo May 13, 2026 01:50
@grunweg
chore: rename fun_prop test files
c3152c3 
After leanprover-community#39261, the only remaining files are fun_prop2.lean and fun_prop_dev.lean.
Rename them to something more telling, and make them UpperCamelCase while
at it. (The latter is mathlib's policy for module names anyway.)
@grunweg grunweg force-pushed the movefunproptest branch from 72f84e3 to c3152c3 Compare May 13, 2026 01:51
@github-actions
Copy link
Copy Markdown

github-actions Bot commented May 13, 2026 •
edited
Loading

PR summary e3960f5cfc

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

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

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.
No changes to weak technical debt.

note: file MathlibTest/fun_prop2.lean` was renamed to `MathlibTest/FunProp.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file MathlibTest/fun_prop_dev.lean` was renamed to `MathlibTest/FunPropMinimal.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

@github-actions github-actions Bot added the file-removed A Lean module was (re)moved without a `deprecated_module` annotation label May 13, 2026
@lecopivo
Copy link
Copy Markdown
Collaborator

lecopivo commented May 13, 2026

Looks good to me!

@grunweg grunweg added the easy < 20s of review time. See the lifecycle page for guidelines. label May 13, 2026
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented May 13, 2026

Randomly rolling reviewers: @YaelDillies would you like to review this? It's very easy.

YaelDillies
YaelDillies approved these changes May 13, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks! 🚀

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions Bot commented May 13, 2026

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

@mathlib-triage mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label May 13, 2026
@bryangingechen
Copy link
Copy Markdown
Contributor

bryangingechen commented May 13, 2026

Thanks!
bors r+

@mathlib-triage mathlib-triage Bot 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 May 13, 2026
mathlib-bors Bot pushed a commit that referenced this pull request May 13, 2026
@grunweg
chore: rename fun_prop test files (#39278)
2d767d6 
After #39261, the only remaining files are fun_prop2.lean and fun_prop_dev.lean. Rename them to something more telling, and make them UpperCamelCase while at it. (The latter is mathlib's policy for module names anyway.)
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors Bot commented May 13, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title chore: rename fun_prop test files [Merged by Bors] - chore: rename fun_prop test files May 13, 2026
@mathlib-bors mathlib-bors Bot closed this May 13, 2026
@grunweg grunweg deleted the movefunproptest branch May 13, 2026 15:50
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@YaelDillies YaelDillies YaelDillies approved these changes

+1 more reviewer

@lecopivo lecopivo lecopivo approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

easy < 20s of review time. See the lifecycle page for guidelines. file-removed A Lean module was (re)moved without a `deprecated_module` annotation ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@grunweg @lecopivo @bryangingechen @YaelDillies