Using {:extern "name"} breaks generated Java code?

[DavePearce]

I'm trying to use Dafny to generate a Java artifact. Using the defaults, my Dafny code generates Java code that compiles and runs. However, the produced package names are not very "java-like" (e.g. package Stack_Compile) rather thanstack (which would normal appropriate for Java). So, I discovered you can use {:extern "name"} to changes things how you want. In theory, that is helping ... but the generated code no longer compiles. Here is the minimal example:

module Test {
  function method inc(x:int) : int {
    x+1
  }
}

Using dafny /compileTarget:java test.dfy, this works fine. However, changing the first line to module {:extern "test"} and it fails with this error:

test-java/test/_ExternBase___default.java:13: error: cannot find symbol
 private static final dafny.TypeDescriptor<__default> _TYPE = ...
                                           ^

As far as I can tell, the issue seems to be that it is generating the file _ExternBase___default.java instead of just __default.java.

Any thoughts appreciated!

[DavePearce]

Perhaps a duplicate of #2155 ?