search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.94k stars 263 forks source link

Omit empty modules when translating to Go #5766

Closed robin-aws closed 2 months ago

robin-aws commented 2 months ago

Description

The empty parent modules of a Dafny module like A.B.C can cause trouble in Go when trying to use --go-module-name - these aren't recorded in translation records since they can appear in multiple compilation units. This may need to be extended to other target languages in the future.

How has this been tested?

GoEmptyParentModules.dfy, which uses CHECK-NOT to assert the empty modules don't show up in the translated code.

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

MikaelMayer commented 2 months ago

How is this PR doing @robin-aws ?

robin-aws commented 2 months ago

Just need to beef up (or tasty-vegetarian-option-up :) the test to actually assert the empty modules aren't emitted, will try to do that today!