Skip to content

Conversation

@eric-wieser
Copy link
Contributor

@eric-wieser eric-wieser commented Oct 15, 2025

Detected by https://clang.llvm.org/extra/clang-tidy/checks/performance/noexcept-move-constructor.html.
This ensures constructions like std::vector<object_ref> call these operators instead of the copy ones, and do not do extra refcounting.

Note that optional and atomic need something more complex using noexcept(), as they are templated.

@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 Oct 15, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Oct 15, 2025

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 4077bf2c05b74a2eaaf1db9be957236f29614f63 --onto 14ff08db6f651775ead432d367b6b083878bb0f9. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-15 10:29:07)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 4077bf2c05b74a2eaaf1db9be957236f29614f63 --onto efbbb0b230ce95653d25b59c83fd24a51a8bf363. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-21 14:18:08)

@leanprover-bot
Copy link
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 4077bf2c05b74a2eaaf1db9be957236f29614f63 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-15 10:29:09)

@eric-wieser eric-wieser marked this pull request as ready for review October 17, 2025 09:42
@eric-wieser eric-wieser changed the title perf: mark move constructors as noexcept perf: mark move constructors and assignement operators as noexcept Oct 17, 2025
@Kha
Copy link
Member

Kha commented Oct 21, 2025

@eric-wieser Is the stage0 change an oversight? We can't merge it the standard way unless it is reverted

@eric-wieser
Copy link
Contributor Author

It was indeed an oversight, now reverted.

@eric-wieser
Copy link
Contributor Author

Note that this and #10815 conflict in a way that git won't pick up; if either is merged, the other will need a small patch to be correct.

@eric-wieser eric-wieser changed the title perf: mark move constructors and assignement operators as noexcept perf: mark move constructors and assignment operators as noexcept Oct 21, 2025
@Kha Kha added this pull request to the merge queue Oct 22, 2025
@Kha
Copy link
Member

Kha commented Oct 22, 2025

@eric-wieser Ok, feel free to update the other PR afterwards. Btw, I suspect a good amount of this code is dead; if you have a tool for that as well, let me know!

Merged via the queue into leanprover:master with commit 08bc333 Oct 22, 2025
20 checks passed
wkrozowski pushed a commit to wkrozowski/lean4 that referenced this pull request Oct 27, 2025
…anprover#10784)

Detected by
https://clang.llvm.org/extra/clang-tidy/checks/performance/noexcept-move-constructor.html.
This ensures constructions like `std::vector<object_ref>` call these
operators instead of the copy ones, and do not do extra refcounting.

Note that `optional` and `atomic` need something more complex using
`noexcept()`, as they are templated.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants