fix: Release lock before raising exception for improved recovery

[fabiomadge]

Fixes #5913.

[keyboardDrummer]

Could you add a test?

[fabiomadge]

I think that's more trouble than it's worth. The map already has tests and this change is just about what I consider undefined behaviour.

[keyboardDrummer]

this change is just about what I consider undefined behaviour.

If I understand correctly, previously you could call Put incorrectly, and then if you catched the error that it throws, any subsequent calls to Put would hang. Did I get that right? I agree it's a corner case, but one that a user ran into and that seems easy to test. Why not add a test to prevent it from re-occurring?

[fabiomadge]

Your understanding is correct. I'm not against adding the test, but I’m not convinced its worth my time.

[fabiomadge]

Let me elaborate on what I meant by undefined behaviour. I can't think of a way of running into this issue from Dafny generated code. I believe the contract with the user stipulates that we provide a correct Dafny library, not one for general consumption from any Python codebase.
I also can't think of a precedent of tests without any Dafny code, so I am hesitant to break with it.

[keyboardDrummer]

Let me elaborate on what I meant by undefined behaviour. I can't think of a way of running into this issue from Dafny generated code. I believe the contract with the user stipulates that we provide a correct Dafny library, not one for general consumption from any Python codebase.

That's fair.

I also can't think of a precedent of tests without any Dafny code, so I am hesitant to break with it.

Me neither. You could use the littish tests for it but it would feel kind of hacky because you'd have a .dfy file with no actualy Dafny instructions, just shell commands to run some Python code.