From 8813a8e6d13a67c8a6ffad5255334af834fabdc7 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Fri, 7 Jul 2023 16:11:00 +0200
Subject: [PATCH 1/8] Add the compile suffix option

---
 Source/DafnyCore/AST/Modules/ModuleDefinition.cs | 5 +++--
 Source/DafnyCore/Options/CommonOptionBag.cs      | 5 +++++
 Source/DafnyCore/Options/ICommandSpec.cs         | 3 ++-
 3 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs
index 5e53a1961ad..22ab1f784d1 100644
--- a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs
+++ b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs
@@ -177,12 +177,13 @@ public string SanitizedName {
   public string GetCompileName(DafnyOptions options) {
     if (compileName == null) {
       var externArgs = options.DisallowExterns ? null : Attributes.FindExpressions(this.Attributes, "extern");
+      var nonExternSuffix = (options.Get(CommonOptionBag.AddCompileSuffix) ? "_Compile" : "");
       if (externArgs != null && 1 <= externArgs.Count && externArgs[0] is StringLiteralExpr) {
         compileName = (string)((StringLiteralExpr)externArgs[0]).Value;
       } else if (externArgs != null) {
-        compileName = Name;
+        compileName = Name + nonExternSuffix;
       } else {
-        compileName = SanitizedName;
+        compileName = SanitizedName + nonExternSuffix;
       }
     }
 
diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs
index cdd3198788e..94b88939fbb 100644
--- a/Source/DafnyCore/Options/CommonOptionBag.cs
+++ b/Source/DafnyCore/Options/CommonOptionBag.cs
@@ -9,6 +9,11 @@ namespace Microsoft.Dafny;
 
 public class CommonOptionBag {
 
+  public static readonly Option<bool> AddCompileSuffix =
+    new("--compile-suffix", "Add the suffix _Compile to module names without :extern") {
+      IsHidden = true
+    };
+  
   public static readonly Option<bool> ManualLemmaInduction =
     new("--manual-lemma-induction", "Turn off automatic induction for lemmas.");
 
diff --git a/Source/DafnyCore/Options/ICommandSpec.cs b/Source/DafnyCore/Options/ICommandSpec.cs
index e7d570783ae..097bb23bdbc 100644
--- a/Source/DafnyCore/Options/ICommandSpec.cs
+++ b/Source/DafnyCore/Options/ICommandSpec.cs
@@ -49,7 +49,8 @@ static ICommandSpec() {
     CommonOptionBag.EnforceDeterminism,
     CommonOptionBag.OptimizeErasableDatatypeWrapper,
     CommonOptionBag.TestAssumptions,
-    DeveloperOptionBag.Bootstrapping
+    DeveloperOptionBag.Bootstrapping,
+    CommonOptionBag.AddCompileSuffix,
   }.Concat(VerificationOptions).ToList();
 
   public static IReadOnlyList<Option> ExecutionOptions = new Option[] {

From b0b4f1d19b106d5e80e74de8e2549c107dddebf9 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Fri, 7 Jul 2023 16:14:39 +0200
Subject: [PATCH 2/8] Add release note

---
 docs/dev/news/4265.feat | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 docs/dev/news/4265.feat

diff --git a/docs/dev/news/4265.feat b/docs/dev/news/4265.feat
new file mode 100644
index 00000000000..6517717c9bc
--- /dev/null
+++ b/docs/dev/news/4265.feat
@@ -0,0 +1 @@
+When translated to other languages, Dafny module names no longer have the suffix `_Compile` appended to them. This may cause issues with existing code from non-Dafny languages in your codebase, if that code was previously referencing modules with `_Compile` in the name. You can migrate either by removing the `_Compile` part of references in your codebase, or by using the backwards compatibility option `--compile-suffix` when using `translate`, `build`, or `run`.
\ No newline at end of file

From 79045a403a3376e6c9f89c71ad7aa27427b23f6d Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Fri, 7 Jul 2023 16:14:53 +0200
Subject: [PATCH 3/8] Run formatter

---
 Source/DafnyCore/Options/CommonOptionBag.cs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs
index 94b88939fbb..cfbd6cd2a81 100644
--- a/Source/DafnyCore/Options/CommonOptionBag.cs
+++ b/Source/DafnyCore/Options/CommonOptionBag.cs
@@ -13,7 +13,7 @@ public class CommonOptionBag {
     new("--compile-suffix", "Add the suffix _Compile to module names without :extern") {
       IsHidden = true
     };
-  
+
   public static readonly Option<bool> ManualLemmaInduction =
     new("--manual-lemma-induction", "Turn off automatic induction for lemmas.");
 

From 2c38fb552960528c01317e43113c4c7bc57216e9 Mon Sep 17 00:00:00 2001
From: Robin Salkeld <salkeldr@amazon.com>
Date: Fri, 7 Jul 2023 09:51:52 -0700
Subject: [PATCH 4/8] Register the new option with DooFile, add to legacy CLI
 as well

---
 Source/DafnyCore/DafnyOptions.cs            | 2 ++
 Source/DafnyCore/Options/CommonOptionBag.cs | 7 +++++++
 2 files changed, 9 insertions(+)

diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs
index 735d12591f1..84a0bd69126 100644
--- a/Source/DafnyCore/DafnyOptions.cs
+++ b/Source/DafnyCore/DafnyOptions.cs
@@ -124,6 +124,8 @@ void ParsePrintMode(Option<PrintModes> option, Bpl.CommandLineParseState ps, Daf
           }
         }
       }
+      
+      RegisterLegacyUi(CommonOptionBag.AddCompileSuffix, ParseBoolean, "Compilation options", "compileSuffix");
     }
 
     public void ApplyBinding(Option option) {
diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs
index cfbd6cd2a81..a4b90aec3db 100644
--- a/Source/DafnyCore/Options/CommonOptionBag.cs
+++ b/Source/DafnyCore/Options/CommonOptionBag.cs
@@ -245,6 +245,10 @@ static CommonOptionBag() {
     DafnyOptions.RegisterLegacyBinding(StdIn, (options, value) => {
       options.UseStdin = value;
     });
+    
+    DafnyOptions.RegisterLegacyBinding(AddCompileSuffix, (options, value) => {
+      // options.UseStdin = value;
+    });
 
     DafnyOptions.RegisterLegacyBinding(FormatPrint, (options, value) => {
       options.DafnyPrintFile = value ? "-" : null;
@@ -295,6 +299,9 @@ static CommonOptionBag() {
         // target language code from referencing compiled internal code,
         // so to be conservative we flag this as not compatible in general.
         { OptimizeErasableDatatypeWrapper, DooFile.CheckOptionMatches },
+        // Similarly this shouldn't matter if external code ONLY refers to {:extern}s,
+        // but in practice it does.
+        { AddCompileSuffix, DooFile.CheckOptionMatches }
       }
     );
     DooFile.RegisterNoChecksNeeded(

From a85225ec73d25d328f8cc1ec179eeeb43339b15c Mon Sep 17 00:00:00 2001
From: Robin Salkeld <salkeldr@amazon.com>
Date: Fri, 7 Jul 2023 10:06:22 -0700
Subject: [PATCH 5/8] Fix to EmitCallToMain for Java (might want to clean up a
 bit)

---
 Source/DafnyCore/Compilers/Java/Compiler-java.cs | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/Source/DafnyCore/Compilers/Java/Compiler-java.cs b/Source/DafnyCore/Compilers/Java/Compiler-java.cs
index 3218376e766..477967033ad 100644
--- a/Source/DafnyCore/Compilers/Java/Compiler-java.cs
+++ b/Source/DafnyCore/Compilers/Java/Compiler-java.cs
@@ -335,7 +335,12 @@ public override void EmitCallToMain(Method mainMethod, string baseName, Concrete
 
       var companion = TypeName_Companion(UserDefinedType.FromTopLevelDeclWithAllBooleanTypeParameters(mainMethod.EnclosingClass), wr, mainMethod.tok, mainMethod);
       var wBody = wr.NewNamedBlock("public static void main(String[] args)");
-      var modName = mainMethod.EnclosingClass.EnclosingModuleDefinition.GetCompileName(Options) == "_module" ? "_System." : "";
+      var addCompileSuffix = Options.Get(CommonOptionBag.AddCompileSuffix);
+      var defaultModuleCompileName = addCompileSuffix ? "_module_Compile" : "_module";
+      var enclosingModuleCompileNAme = mainMethod.EnclosingClass.EnclosingModuleDefinition.GetCompileName(Options);
+      var modName = enclosingModuleCompileNAme == defaultModuleCompileName 
+        ? (addCompileSuffix ? "_System_Compile." : "_System.")
+        : "";
       companion = modName + companion;
       Coverage.EmitSetup(wBody);
       wBody.WriteLine($"{DafnyHelpersClass}.withHaltHandling(() -> {{ {companion}.__Main({DafnyHelpersClass}.{CharMethodQualifier}FromMainArguments(args)); }} );");

From c2767c18a0dd2238f7f4b0b04fe7bb70ed9d8d37 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Sat, 8 Jul 2023 18:10:03 +0200
Subject: [PATCH 6/8] Fix Options.txt and run formatter

---
 Source/DafnyCore/DafnyOptions.cs            | 2 +-
 Source/DafnyCore/Options/CommonOptionBag.cs | 2 +-
 docs/DafnyRef/Options.txt                   | 3 +++
 3 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs
index 84a0bd69126..5e81545f248 100644
--- a/Source/DafnyCore/DafnyOptions.cs
+++ b/Source/DafnyCore/DafnyOptions.cs
@@ -124,7 +124,7 @@ void ParsePrintMode(Option<PrintModes> option, Bpl.CommandLineParseState ps, Daf
           }
         }
       }
-      
+
       RegisterLegacyUi(CommonOptionBag.AddCompileSuffix, ParseBoolean, "Compilation options", "compileSuffix");
     }
 
diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs
index a4b90aec3db..81de8686133 100644
--- a/Source/DafnyCore/Options/CommonOptionBag.cs
+++ b/Source/DafnyCore/Options/CommonOptionBag.cs
@@ -245,7 +245,7 @@ static CommonOptionBag() {
     DafnyOptions.RegisterLegacyBinding(StdIn, (options, value) => {
       options.UseStdin = value;
     });
-    
+
     DafnyOptions.RegisterLegacyBinding(AddCompileSuffix, (options, value) => {
       // options.UseStdin = value;
     });
diff --git a/docs/DafnyRef/Options.txt b/docs/DafnyRef/Options.txt
index d12938f11c3..e5ce095472f 100644
--- a/docs/DafnyRef/Options.txt
+++ b/docs/DafnyRef/Options.txt
@@ -348,6 +348,9 @@ Usage: dafny [ option ... ] [ filename ... ]
       Disable axiom pruning that Dafny uses to speed up verification.
   ---- Compilation options ---------------------------------------------------
   
+  /compileSuffix:<value>
+      Add the suffix _Compile to module names without :extern
+
   /compileTarget:<language>
       cs (default) - Compile to .NET via C#.
       go - Compile to Go.

From 871205d091af1d771eb638bfef52f748aef1027d Mon Sep 17 00:00:00 2001
From: Robin Salkeld <salkeldr@amazon.com>
Date: Sat, 8 Jul 2023 11:50:36 -0700
Subject: [PATCH 7/8] Revert no-op legacy binding

---
 Source/DafnyCore/Options/CommonOptionBag.cs | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs
index 81de8686133..228ed28284a 100644
--- a/Source/DafnyCore/Options/CommonOptionBag.cs
+++ b/Source/DafnyCore/Options/CommonOptionBag.cs
@@ -246,10 +246,6 @@ static CommonOptionBag() {
       options.UseStdin = value;
     });
 
-    DafnyOptions.RegisterLegacyBinding(AddCompileSuffix, (options, value) => {
-      // options.UseStdin = value;
-    });
-
     DafnyOptions.RegisterLegacyBinding(FormatPrint, (options, value) => {
       options.DafnyPrintFile = value ? "-" : null;
     });

From 21987c87bdc108fe99f5c8b216b8be7c77a6f0c7 Mon Sep 17 00:00:00 2001
From: Robin Salkeld <salkeldr@amazon.com>
Date: Sat, 8 Jul 2023 14:12:42 -0700
Subject: [PATCH 8/8] Whitespace

---
 Source/DafnyCore/Compilers/Java/Compiler-java.cs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Source/DafnyCore/Compilers/Java/Compiler-java.cs b/Source/DafnyCore/Compilers/Java/Compiler-java.cs
index 477967033ad..459e03508b5 100644
--- a/Source/DafnyCore/Compilers/Java/Compiler-java.cs
+++ b/Source/DafnyCore/Compilers/Java/Compiler-java.cs
@@ -338,7 +338,7 @@ public override void EmitCallToMain(Method mainMethod, string baseName, Concrete
       var addCompileSuffix = Options.Get(CommonOptionBag.AddCompileSuffix);
       var defaultModuleCompileName = addCompileSuffix ? "_module_Compile" : "_module";
       var enclosingModuleCompileNAme = mainMethod.EnclosingClass.EnclosingModuleDefinition.GetCompileName(Options);
-      var modName = enclosingModuleCompileNAme == defaultModuleCompileName 
+      var modName = enclosingModuleCompileNAme == defaultModuleCompileName
         ? (addCompileSuffix ? "_System_Compile." : "_System.")
         : "";
       companion = modName + companion;