From 9cac1dc40e7ebf7564561ca049a2532a0dc73c37 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 9 Aug 2024 13:50:00 -0700 Subject: [PATCH] Comment --- .../java/src/main/java/String_Compile/__default.java | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/StandardLibrary/runtimes/java/src/main/java/String_Compile/__default.java b/StandardLibrary/runtimes/java/src/main/java/String_Compile/__default.java index c459b8322..ddc8ec2c0 100644 --- 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() {