fix: Block .doo files as input in legacy CLI (#3967)

Also use the new CLI when executing Dafny files for the library and
Simple Dafny backends.

Author: robin-aws

Source/DafnyCore/Compilers/Dafny/DafnyBackend.cs

@@ -45,7 +45,7 @@ public override bool RunTargetProgram(string dafnyProgramName, string targetProg
     string targetFilename, ReadOnlyCollection<string> otherFileNames, object compilationResult, TextWriter outputWriter) {
     Contract.Requires(targetFilename != null || otherFileNames.Count == 0);
 
-    return RunTargetDafnyProgram(targetFilename, outputWriter);
+    return RunTargetDafnyProgram(targetFilename, outputWriter, false);
   }
 
   public DafnyBackend(DafnyOptions options) : base(options) {

Source/DafnyCore/Compilers/ExecutableBackend.cs

@@ -116,7 +116,7 @@ protected static void WriteFromFile(string inputFilename, TextWriter outputWrite
     SinglePassCompiler.WriteFromStream(rd, outputWriter);
   }
 
-  protected bool RunTargetDafnyProgram(string targetFilename, TextWriter outputWriter) {
+  protected bool RunTargetDafnyProgram(string targetFilename, TextWriter outputWriter, bool verify) {
 
     /*
      * In order to work for the continuous integration, we need to call the Dafny compiler using dotnet
@@ -128,15 +128,17 @@ protected bool RunTargetDafnyProgram(string targetFilename, TextWriter outputWri
     var dafny = where + "/Dafny.dll";
 
     var opt = Options;
-    var psi = PrepareProcessStartInfo("dotnet", opt.MainArgs
-      .Prepend("/compileTarget:cs")
-      .Prepend("/compile:4")
-      .Prepend("/compileVerbose:0")
-      .Prepend("/printVerifiedProceduresCount:0")
-      .Prepend("/noVerify")
-      .Prepend(targetFilename)
-      .Prepend(dafny));
-
+    var args = opt.MainArgs
+      .Prepend(targetFilename);
+    if (!verify) {
+      args = args.Prepend("--no-verify");
+    }
+    args = args
+      .Prepend("--target:cs")
+      .Prepend("run")
+      .Prepend(dafny);
+    var psi = PrepareProcessStartInfo("dotnet", args);
+    Console.Out.WriteLine(string.Join(", ", psi.ArgumentList));
     /*
      * When this code was written, the Dafny compiler cannot be made completely silent.
      * This is a problem for this specific compiler and the integration tests because the second

Source/DafnyCore/Compilers/Library/LibraryBackend.cs

@@ -83,6 +83,6 @@ public override bool RunTargetProgram(string dafnyProgramName, string targetProg
     ReadOnlyCollection<string> otherFileNames, object compilationResult, TextWriter outputWriter) {
 
     var dooPath = DooFilePath(dafnyProgramName);
-    return RunTargetDafnyProgram(dooPath, outputWriter);
+    return RunTargetDafnyProgram(dooPath, outputWriter, true);
   }
 }

Source/DafnyCore/DooFile.cs

@@ -113,6 +113,11 @@ private DooFile() {
   }
 
   public bool Validate(string filePath, DafnyOptions options, Command currentCommand) {
+    if (currentCommand == null) {
+      options.Printer.ErrorWriteLine(Console.Out, $"Cannot load {filePath}: .doo files cannot be used with the legacy CLI");
+      return false;
+    }
+
     if (options.VersionNumber != Manifest.DafnyVersion) {
       options.Printer.ErrorWriteLine(Console.Out, $"Cannot load {filePath}: it was built with Dafny {Manifest.DafnyVersion}, which cannot be used by Dafny {options.VersionNumber}");
       return false;