Add the compile suffix option

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;
       }
     }
 

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)); }} );");

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) {

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.");
 
@@ -290,6 +295,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(

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[] {

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.

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`.