Skip to content

fix: use assignment to implement optional<> move assignment #10815

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
eric-wieser wants to merge 3 commits into
base: master
Choose a base branch
from
Open

fix: use assignment to implement optional<> move assignment #10815

eric-wieser wants to merge 3 commits into from

Conversation

@eric-wieser
Copy link
Contributor

@eric-wieser eric-wieser commented Oct 17, 2025 •
edited
Loading

This PR ensures that when reassigning an already-assigned optional, the underlying move or copy assignment operator is used rather than destructing and constructing. This matches std::optional.

This also fixes an exception safety bug where o1 = o2 for optional<T> would leave o1 in an invalid state if the copy constructor for T throws.

As a reminder, we can't use the upstream std::optional until C++17.

eric-wieser
eric-wieser commented Oct 17, 2025
View reviewed changes
@eric-wieser eric-wieser force-pushed the fix-optional-assignment branch 7 times, most recently from 36bedbf to 8ebec37 Compare October 21, 2025 13:22
@eric-wieser eric-wieser changed the title perf: use assignment to implement optional<> move assignment fix: use assignment to implement optional<> move assignment Oct 21, 2025
@eric-wieser
Copy link
Contributor Author

eric-wieser commented Oct 21, 2025

changelog-none

@github-actions github-actions bot added changelog-none toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN labels Oct 21, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Oct 21, 2025 •
edited
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 2f90b1dadd0fbf6adfda4045f55189c8b74421b2 --onto efbbb0b230ce95653d25b59c83fd24a51a8bf363. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-21 14:34:34)
  • ✅ Mathlib branch lean-pr-testing-10815 has successfully built against this PR. (2025-11-11 14:36:07) View Log
  • ✅ Mathlib branch lean-pr-testing-10815 has successfully built against this PR. (2025-12-03 05:23:33) View Log

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Oct 21, 2025 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 2f90b1dadd0fbf6adfda4045f55189c8b74421b2 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-21 14:34:36)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-11-07 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-11-11 13:37:56)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-12-01 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-12-03 04:17:45)

@eric-wieser eric-wieser mentioned this pull request Oct 21, 2025
Merged
@eric-wieser eric-wieser force-pushed the fix-optional-assignment branch from 8ebec37 to 7785558 Compare November 7, 2025 22:58
eric-wieser
eric-wieser commented Nov 7, 2025
View reviewed changes
src/runtime/optional.h
m_value.~T();
m_some = true;
new (&m_value) T(std::move(other));
optional& operator=(T && other) {
Copy link
Contributor Author

@eric-wieser eric-wieser Nov 7, 2025

Choose a reason for hiding this comment

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

This one was unecessarily noexcept, std::optional does not mark it as such.

@eric-wieser eric-wieser force-pushed the fix-optional-assignment branch from 7785558 to a8bfe15 Compare November 7, 2025 23:27
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 11, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#10815
cc9a907
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Nov 11, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#10815
965222a
@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Nov 11, 2025
Kha
Kha requested changes Nov 25, 2025
View reviewed changes
Copy link
Member

@Kha Kha left a comment

Choose a reason for hiding this comment

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

Could you please merge master so that we can also run the new fsanitize job on this?

@leanprover-bot leanprover-bot added the P-medium We may work on this issue if we find the time label Dec 1, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Dec 3, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10815
eff037e
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Dec 3, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10815
5fec2fb
@eric-wieser
Copy link
Contributor Author

eric-wieser commented Dec 4, 2025

changelog-skip

@eric-wieser
Copy link
Contributor Author

eric-wieser commented Dec 4, 2025

changelog-no

@github-actions github-actions bot added changelog-no Do not include this PR in the release changelog and removed changelog-skip labels Dec 4, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@Kha Kha Kha requested changes

Assignees

No one assigned

Labels

builds-mathlib CI has verified that Mathlib builds against this PR changelog-no Do not include this PR in the release changelog P-medium We may work on this issue if we find the time 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

@eric-wieser @leanprover-community-bot @leanprover-bot @Kha