Skip to content

chore: fix naming of several theorems#7499

Merged
TwoFX merged 18 commits intoleanprover:masterfrom
Rob23oba:naming-fixes
Apr 4, 2025
Merged

chore: fix naming of several theorems#7499
TwoFX merged 18 commits intoleanprover:masterfrom
Rob23oba:naming-fixes

Conversation

@Rob23oba
Copy link
Copy Markdown
Contributor

@Rob23oba Rob23oba commented Mar 15, 2025

This PR fixes the spelling of several theorems to adhere to the naming convention.

Note: The changes here were found using a tool.

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Mar 15, 2025
@ghost
Copy link
Copy Markdown

ghost commented Mar 15, 2025 •
edited by ghost
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a788e6aa6730ea901e17391c765d0b2508586bc5 --onto d5f01f2db1efd18034421ae2f40120d1c608f3c0. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-15 13:19:35)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5e0648fe988ccb6d25f369227daf21d78ce3030c --onto d32a7b250ad20477d55034488d89a050fbf70af5. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-17 18:08:23)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 53fcae031e5a37c7d8c0ac880f4da28929e3b932 --onto d32a7b250ad20477d55034488d89a050fbf70af5. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-18 17:02:45)
  • 💥 Mathlib branch lean-pr-testing-7499 build failed against this PR. (2025-03-19 16:33:25) View Log
  • 💥 Mathlib branch lean-pr-testing-7499 build failed against this PR. (2025-04-03 11:09:21) View Log
  • 🟡 Mathlib branch lean-pr-testing-7499 build against this PR was cancelled. (2025-04-03 15:17:15) View Log
  • ✅ Mathlib branch lean-pr-testing-7499 has successfully built against this PR. (2025-04-03 15:54:12) View Log
  • ✅ Mathlib branch lean-pr-testing-7499 has successfully built against this PR. (2025-04-04 09:44:09) View Log

@TwoFX TwoFX self-assigned this Mar 15, 2025
@TwoFX
Copy link
Copy Markdown
Member

TwoFX commented Mar 17, 2025 •
edited
Loading

Thanks for doing this! I haven't gone through all files yet, but everything I've seen so far is looking great. I am assuming that the fallout in mathlib will be substantial, and there needs to be a mathlib branch ready for us to be able to merge this. At the same time this PR will accumulate marge conflicts quickly, so I suggest you try to rebase and get mathlib building quickly (and I'll be quick about merging once mathlib is building), possibly deferring the BitVec changes to a future PR to avoid merge conflicts here in core.

Update: I've gone through everything now, so I'm ready to hit merge once we have a mathlib build.

@Kha Kha added the awaiting-author Waiting for PR author to address issues label Mar 18, 2025
@Rob23oba Rob23oba force-pushed the naming-fixes branch 3 times, most recently from 91aaa32 to 7c9a084 Compare March 19, 2025 14:08
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Mar 19, 2025
Update lean-toolchain for testing leanprover/lean4#7499
7456847
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 19, 2025
Update lean-toolchain for testing leanprover/lean4#7499
142d7dd
@ghost ghost added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Mar 19, 2025
@TwoFX TwoFX mentioned this pull request Mar 31, 2025
Closed
3 tasks
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 3, 2025
Trigger CI for leanprover/lean4#7499
97d5a31
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 3, 2025
Trigger CI for leanprover/lean4#7499
3ec311d
@ghost ghost added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Apr 3, 2025
@github-actions github-actions bot added awaiting-review Waiting for someone to review the PR and removed awaiting-author Waiting for PR author to address issues labels Apr 4, 2025
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 4, 2025
Trigger CI for leanprover/lean4#7499
73f6780
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 4, 2025
Trigger CI for leanprover/lean4#7499
e18c355
TwoFX
TwoFX approved these changes Apr 4, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@TwoFX TwoFX left a comment

Choose a reason for hiding this comment

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

Superb, thanks!

@TwoFX TwoFX added this pull request to the merge queue Apr 4, 2025
Merged via the queue into leanprover:master with commit 575e030 Apr 4, 2025
16 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@TwoFX TwoFX TwoFX approved these changes

@hargoniX hargoniX Awaiting requested review from hargoniX hargoniX is a code owner

@digama0 digama0 Awaiting requested review from digama0 digama0 is a code owner

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees

@TwoFX TwoFX

Labels

awaiting-review Waiting for someone to review the PR builds-mathlib CI has verified that Mathlib builds against this PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@Rob23oba @TwoFX @Kha @ashandoak