Standard libraries and separate compilation

Source/DafnyCore/Backends/CSharp/CsharpBackend.cs

@@ -1,8 +1,10 @@
+using System;
 using System.Collections.Generic;
 using System.Collections.ObjectModel;
 using System.IO;
 using System.Reflection;
 using System.Text;
+using System.Threading;
 using System.Threading.Tasks;
 
 namespace Microsoft.Dafny.Compilers;
@@ -131,7 +133,10 @@ public override async Task<bool> RunTargetProgram(string dafnyProgramName, strin
 
     foreach (var otherFileName in otherFileNames) {
       if (Path.GetExtension(otherFileName) == ".dll") {
-        File.Copy(otherFileName, Path.Combine(dllFolder, Path.GetFileName(otherFileName)), true);
+        var destination = Path.Combine(dllFolder, Path.GetFileName(otherFileName));
+        if (Path.GetFullPath(otherFileName) != Path.GetFullPath(destination)) {
+          File.Copy(otherFileName, destination, true);
+        }
       }
     }
 

Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs

@@ -97,7 +97,7 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {
       if (Options.IncludeRuntime) {
         EmitRuntimeSource("DafnyRuntimeCsharp", wr, false);
       }
-      if (Options.Get(CommonOptionBag.UseStandardLibraries)) {
+      if (Options.Get(CommonOptionBag.UseStandardLibraries) && Options.Get(CommonOptionBag.TranslateStandardLibrary)) {
         EmitRuntimeSource("DafnyStandardLibraries_cs", wr, false);
       }
 

Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs

@@ -97,7 +97,7 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {
       }
       ImportsNotFromDafnyModules.Add(new Import { Name = "_dafny", Path = $"{path}dafny" });
 
-      if (Options.Get(CommonOptionBag.UseStandardLibraries)) {
+      if (Options.Get(CommonOptionBag.UseStandardLibraries) && Options.Get(CommonOptionBag.TranslateStandardLibrary)) {
         EmitRuntimeSource("DafnyStandardLibraries_go", wr);
       }
 

Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs

@@ -304,7 +304,7 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {
       if (Options.IncludeRuntime) {
         EmitRuntimeSource("DafnyRuntimeJava", wr);
       }
-      if (Options.Get(CommonOptionBag.UseStandardLibraries)) {
+      if (Options.Get(CommonOptionBag.UseStandardLibraries) && Options.Get(CommonOptionBag.TranslateStandardLibrary)) {
         EmitRuntimeSource("DafnyStandardLibraries_java", wr);
       }
       wr.WriteLine($"// Dafny program {program.Name} compiled into Java");

Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs

@@ -47,7 +47,7 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {
       if (Options.IncludeRuntime) {
         EmitRuntimeSource("DafnyRuntimeJs", wr, false);
       }
-      if (Options.Get(CommonOptionBag.UseStandardLibraries)) {
+      if (Options.Get(CommonOptionBag.UseStandardLibraries) && Options.Get(CommonOptionBag.TranslateStandardLibrary)) {
         EmitRuntimeSource("DafnyStandardLibraries_js", wr, false);
       }
     }

Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs

@@ -69,7 +69,7 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {
       if (Options.IncludeRuntime) {
         EmitRuntimeSource("DafnyRuntimePython", wr);
       }
-      if (Options.Get(CommonOptionBag.UseStandardLibraries)) {
+      if (Options.Get(CommonOptionBag.UseStandardLibraries) && Options.Get(CommonOptionBag.TranslateStandardLibrary)) {
         EmitRuntimeSource("DafnyStandardLibraries_py", wr);
       }
 

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -366,6 +366,12 @@ public enum DefaultFunctionOpacityOptions {
 `opaque` means functions are always opaque so the opaque keyword is not needed, and functions must be revealed everywhere needed for a proof.".TrimStart()) {
   };
 
+  public static readonly Option<bool> TranslateStandardLibrary = new("--translate-standard-library", () => true,
+    @"Currently Dafny does not prevent separately built Dafny projects from each including the standard library,
+leading to conflicts. When combining such projects, please ensure that only one of them has --translate-standard-library set to true.
+When building a Dafny library (.doo file), this option will automatically be set to false. 
+");
+
   public static readonly Option<bool> UseStandardLibraries = new("--standard-libraries", () => false,
     @"
 Allow Dafny code to depend on the standard libraries included with the Dafny distribution.
@@ -610,6 +616,7 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
     OptionRegistry.RegisterGlobalOption(AllowDeprecation, OptionCompatibility.OptionLibraryImpliesLocalWarning);
     OptionRegistry.RegisterGlobalOption(WarnShadowing, OptionCompatibility.OptionLibraryImpliesLocalWarning);
     OptionRegistry.RegisterGlobalOption(UseStandardLibraries, OptionCompatibility.OptionLibraryImpliesLocalError);
+    OptionRegistry.RegisterOption(TranslateStandardLibrary, OptionScope.Cli);
     OptionRegistry.RegisterOption(WarnAsErrors, OptionScope.Cli);
     OptionRegistry.RegisterOption(ProgressOption, OptionScope.Cli);
     OptionRegistry.RegisterOption(LogLocation, OptionScope.Cli);

Source/DafnyCore/Options/DafnyCommands.cs

@@ -102,6 +102,7 @@ static DafnyCommands() {
     CommonOptionBag.NewTypeInferenceDebug,
     Method.ReadsClausesOnMethods,
     CommonOptionBag.UseStandardLibraries,
+    CommonOptionBag.TranslateStandardLibrary,
     CommonOptionBag.LogLevelOption,
     CommonOptionBag.LogLocation
   });

Source/DafnyCore/Pipeline/Compilation.cs

@@ -3,13 +3,15 @@
 using System;
 using System.Collections.Concurrent;
 using System.Collections.Generic;
+using System.CommandLine;
 using System.IO;
 using System.Linq;
 using System.Reactive;
 using System.Reactive.Subjects;
 using System.Threading;
 using System.Threading.Tasks;
 using Microsoft.Boogie;
+using Microsoft.Dafny.Compilers;
 using Microsoft.Extensions.Logging;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 using VC;
@@ -176,9 +178,13 @@ private async Task<IReadOnlyList<DafnyFile>> DetermineRootFiles() {
     }
 
     if (Options.Get(CommonOptionBag.UseStandardLibraries)) {
+      if (Options.Backend is LibraryBackend) {
+        Options.Set(CommonOptionBag.TranslateStandardLibrary, false);
+      }
+
       // For now the standard libraries are still translated from scratch.
       // This breaks separate compilation and will be addressed in https://github.com/dafny-lang/dafny/pull/4877
-      var asLibrary = false;
+      var asLibrary = !Options.Get(CommonOptionBag.TranslateStandardLibrary);
 
       if (Options.CompilerName is null or "cs" or "java" or "go" or "py" or "js") {
         var targetName = Options.CompilerName ?? "notarget";

Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs

@@ -197,9 +197,13 @@ public static async Task<int> Run(DafnyOptions options) {
       // only because if they are added first, one might be used as the program name,
       // which is not handled well.
       if (options.Get(CommonOptionBag.UseStandardLibraries)) {
+        if (options.Backend is LibraryBackend) {
+          options.Set(CommonOptionBag.TranslateStandardLibrary, false);
+        }
+
         // For now the standard libraries are still translated from scratch.
         // This breaks separate compilation and will be addressed in https://github.com/dafny-lang/dafny/pull/4877
-        var asLibrary = false;
+        var asLibrary = !options.Get(CommonOptionBag.TranslateStandardLibrary);
 
         var reporter = new ConsoleErrorReporter(options);
         if (options.CompilerName is null or "cs" or "java" or "go" or "py" or "js") {

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/standard-libaries/Inputs/library.dfy

@@ -0,0 +1,8 @@
+module UsesWrappers {
+
+  import opened Std.Wrappers
+
+  function SafeDiv(a: int, b: int): Option<int> {
+    if b == 0 then None else Some(a/b)
+  }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/standard-libaries/user.dfy

@@ -0,0 +1,17 @@
+// NONUNIFORM: Test is too complex for the uniform back-end testing mechanism
+// RUN: %build --target=lib "%S/Inputs/library.dfy" --standard-libraries=true --output %S/Outputs > %t
+// RUN: %run --standard-libraries=true %s --input "%S/Outputs.doo" >> %t
+//
+// Let's pretend we're vending a Dafny library outside of Dafny, and we want to include the std-lib with the library,
+// since the external user won't include it
+// RUN: %build "%S/Inputs/library.dfy" --standard-libraries=true --output %S/Outputs >> %t
+// RUN: %run --standard-libraries=true %s --library "%S/Outputs.doo" --input "%S/Outputs.dll" --translate-standard-library=false >> %t
+// RUN: %diff "%s.expect" "%t"
+
+import opened UsesWrappers
+
+method Main() {
+  print SafeDiv(4, 2), "\n";
+  print SafeDiv(7, 0), "\n";
+}
+

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/standard-libaries/user.dfy.expect

@@ -0,0 +1,12 @@
+
+Dafny program verifier finished with 1 verified, 0 errors
+
+Dafny program verifier finished with 0 verified, 0 errors
+Wrappers.Option.Some(2)
+Wrappers.Option.None
+
+Dafny program verifier finished with 1 verified, 0 errors
+
+Dafny program verifier finished with 0 verified, 0 errors
+Wrappers.Option.Some(2)
+Wrappers.Option.None