Translation records should not include options for empty models #5459
Assignees
Labels
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
release-blocker
Must be resolved before the next release
Comments
robin-aws
added
the
kind: enhancement
keyboardDrummer
pushed a commit
that referenced
this issue
May 22, 2024
### Description Fixes #5459 Omits modules that only contain other modules from translation records, since they can appear in multiple different separately-compiled libraries when they are prefix modules (i.e. a module `A.B` that only appears in a `module A.B.C { ... }` declaration). I attempted to omit such modules from translation entirely at first, but hit issues in the Go backend. It may be possible to do so in the future with more care. ### How has this been tested? Updated `DuplicateModules.dfy` to include parent modules. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
When loading
.dtrfiles, there is a check that a module does not appear more than once in any such file. But it is possible for a prefix module to appear in multiple libraries without any actual conflict (i.e. the moduleA.Bin the snippetmodule A.B.C { ... }. The error you get when something likeA.Bappears multiple times is spurious.The best deeper fix seems to be to not translate empty modules at all, since emitting a declaration of a target language module/package/etc will likely cause target language tooling errors as well.
The text was updated successfully, but these errors were encountered: