Skip to content
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.

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

fix: Drop SelectOpt from MutableMap #162

Merged
merged 4 commits into from
Nov 14, 2024
Merged

fix: Drop SelectOpt from MutableMap #162

merged 4 commits into from
Nov 14, 2024

Conversation

ShubhamChaturvedi7
Copy link
Collaborator

@ShubhamChaturvedi7 ShubhamChaturvedi7 commented Nov 14, 2024

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

Drops SelectOpt from MutableMap: https://t.corp.amazon.com/e502d5d5-8d37-4249-bba6-60fe3545a6ea/communication#899a85f9-9b66-418f-90d0-ee0505811d2e

@ShubhamChaturvedi7 ShubhamChaturvedi7 marked this pull request as ready for review November 14, 2024 21:52
@robin-aws
Copy link
Member

Since the link is not publicly accessible, for the record here's my comment that led us here:

FWIW the copy of MutableMap we include in the Dafny standard libraries avoids this [not being able to implement the class in Go] by not defining any functions/method in Dafny - it doesn't have the problematic SelectOpt helper function: https://github.com/dafny-lang/dafny/blob/master/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-notarget-java-cs-js-go-py.dfy#L70

Although I know we are intending to replace the dafny-lang/libraries submodule with a dafny-lang/dafny submodule so you can use the maintained standard library code, I also know that's going to take substantial work. So I'd suggest as a short term solution we modify libraries to remove the SelectOpt function, since the MPL isn't using it, so that it's possible to implement that MutableMap class in all target languages. Would that work for you?

Copy link
Member

@MikaelMayer MikaelMayer left a comment

Choose a reason for hiding this comment

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

Looks good

@MikaelMayer MikaelMayer merged commit 4b8201a into master Nov 14, 2024
4 checks passed
@MikaelMayer MikaelMayer deleted the mutable_map_fix branch November 14, 2024 23:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants