Comment

aws · Aug 9, 2024 · 9cac1dc · 9cac1dc
1 parent 7bdd6f0
commit 9cac1dc
Showing 1 changed file with 8 additions and 0 deletions.
diff --git a/StandardLibrary/runtimes/java/src/main/java/String_Compile/__default.java b/StandardLibrary/runtimes/java/src/main/java/String_Compile/__default.java
@@ -1,7 +1,15 @@
 package String_Compile;
 
 /**
+ * This is a thunk for the actual Dafny-generated StandardLibrary_mString_Compile.__default class.
  * 
+ * The module names generated for Java changed between Dafny 4.2 and 4.7,
+ * and although `--legacy-module-names` mostly retains the old names,
+ * StandardLibrary.String was previously compiled to String_Compile instead of the expected
+ * StandardLibrary_mString_Compile because of a bug,
+ * and it would have been very difficult to reproduce the exact bug behavior with `--legacy-module-names`.
+ * 
+ * Instead we just create an "alias" for this case.
  */
 public class __default {
   public __default() {