Unqualified reference to module constant from extern-ed class doesn't compile in Java #634
Labels
area: ffi
The {:extern} attribute and otherwise interfacing with code in other languages
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
lang: java
Dafny's Java transpiler and its runtime
part: code-generation
Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
priority: not yet
Will reconsider working on this when we're looking for work
Repro:
The Dafny-to-Java compiler produces
__default.FOO
for the constant reference in the constructor, which doesn't resolve because theFOO
constant is defined inM_Compile._ExternBase___default.java
. The fix is to manually define an empty__default
class:This is a side-effect of the mechanism for mixed Dafny/Java classes as described in #469, but calling this out separately because it's especially difficult to recognize that modules need the same empty subclass.
The text was updated successfully, but these errors were encountered: