search

dafny-lang / libraries

Libraries useful for Dafny programs
Other
43 stars 25 forks source link

fix: Drop SelectOpt from MutableMap #162

Closed ShubhamChaturvedi7 closed 2 weeks ago

ShubhamChaturvedi7 commented 2 weeks ago

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

robin-aws commented 2 weeks ago

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?