Chore: Support for --do-boogie-translation

And not activated by default if `--no-verify` is set. This option emulates the `/dafnyVerify` command in the previous CLI
Added tests

Source/DafnyCore/Options/BoogieOptionBag.cs

@@ -46,6 +46,8 @@ public static class BoogieOptionBag {
 
   public static readonly Option<bool> NoVerify = new("--no-verify", "Skip verification");
 
+  public static readonly Option<bool> DoBoogieTranslation = new("--do-boogie-translation", "Requires --no-verify. Does translation to Boogie but Boogie won't verify it.");
+
   public static readonly Option<bool> HiddenNoVerify = new("--hidden-no-verify",
     "Allows building unverified libraries without recording that they were not verified.") {
     IsHidden = true
@@ -107,9 +109,14 @@ static BoogieOptionBag() {
     });
     DafnyOptions.RegisterLegacyBinding(Cores,
       (o, f) => o.VcsCores = f == 0 ? (1 + System.Environment.ProcessorCount) / 2 : (int)f);
-    DafnyOptions.RegisterLegacyBinding(NoVerify, (options, value) => {
-      var shouldVerify = !value && !options.Get(HiddenNoVerify);
-      options.Verify = shouldVerify;
+    DafnyOptions.RegisterLegacyBinding(NoVerify, (options, dotNotVerify) => {
+      var shouldVerify = !dotNotVerify && !options.Get(HiddenNoVerify);
+      options.Verify = shouldVerify; // Boogie won't verify
+    });
+    // Previously /dafnyVerify
+    DafnyOptions.RegisterLegacyBinding(DoBoogieTranslation, (options, doBoogieTranslation) => {
+      options.DafnyVerify = (!options.Get(NoVerify) && !options.Get(HiddenNoVerify))
+        || doBoogieTranslation || options.Get(DeveloperOptionBag.BoogiePrint) != null; // Dafny won't translate the code to Boogie
     });
     DafnyOptions.RegisterLegacyBinding(VerificationTimeLimit, (o, f) => o.TimeLimit = f);
 
@@ -144,6 +151,7 @@ static BoogieOptionBag() {
 
     OptionRegistry.RegisterGlobalOption(BoogieArguments, OptionCompatibility.CheckOptionMatches);
     OptionRegistry.RegisterGlobalOption(NoVerify, OptionCompatibility.OptionLibraryImpliesLocalError);
+    OptionRegistry.RegisterGlobalOption(DoBoogieTranslation, OptionCompatibility.OptionLibraryImpliesLocalError);
     OptionRegistry.RegisterOption(HiddenNoVerify, OptionScope.Cli);
     OptionRegistry.RegisterOption(Cores, OptionScope.Cli);
     OptionRegistry.RegisterOption(VerificationTimeLimit, OptionScope.Cli);

Source/DafnyCore/Options/DafnyCommands.cs

@@ -52,6 +52,7 @@ static DafnyCommands() {
 
   public static readonly IReadOnlyList<Option> TranslationOptions = new Option[] {
     BoogieOptionBag.NoVerify,
+    BoogieOptionBag.DoBoogieTranslation,
     BoogieOptionBag.HiddenNoVerify,
     CommonOptionBag.OptimizeErasableDatatypeWrapper,
     CommonOptionBag.TestAssumptions,

Source/DafnyDriver.Test/OptionsTest.cs

@@ -0,0 +1,72 @@
+using System.CommandLine;
+using System.CommandLine.Builder;
+using System.CommandLine.Invocation;
+using System.CommandLine.Parsing;
+using System.Diagnostics;
+using System.IO.Pipelines;
+using System.Reactive.Concurrency;
+using System.Reflection;
+using System.Text;
+using Microsoft.Dafny;
+using Microsoft.Extensions.Logging.Abstractions;
+using OmniSharp.Extensions.JsonRpc;
+using OmniSharp.Extensions.JsonRpc.Client;
+using OmniSharp.Extensions.JsonRpc.Serialization;
+using OmniSharp.Extensions.LanguageServer.Protocol.Client.Capabilities;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
+using XunitAssertMessages;
+using Command = System.CommandLine.Command;
+
+namespace DafnyDriver.Test;
+
+
+public class OptionsTest {
+  [Fact]
+  public async Task RunFlagsOverride() {
+    await TestCliRunArgs([], options => {
+      Assert.True(options.DafnyVerify);
+      Assert.True(options.Verify);
+      return 0;
+    });
+    await TestCliRunArgs(["--no-verify"], options => {
+      Assert.False(options.DafnyVerify);
+      Assert.False(options.Verify);
+      return 0;
+    });
+    await TestCliRunArgs(["--no-verify", "--do-boogie-translation"], options => {
+      Assert.True(options.DafnyVerify);
+      Assert.False(options.Verify);
+      return 0;
+    });
+    await TestCliRunArgs(["--no-verify", "--bprint=-"], options => {
+      Assert.True(options.DafnyVerify);
+      Assert.False(options.Verify);
+      return 0;
+    });
+  }
+
+  private static async Task TestCliRunArgs(string[] cmdArgs, Func<DafnyOptions, int> optionsCallback) {
+    var fullArgs = new string[] {
+      "run"
+    };
+    fullArgs = fullArgs.Concat(cmdArgs).Concat(new string[] { "file.dfy" }).ToArray();
+    var callbackCalled = false;
+    var newOptionsCallback = (DafnyOptions options) => {
+      callbackCalled = true;
+      return optionsCallback(options);
+    };
+    Command cmd = RunCommand.Create(newOptionsCallback);
+    var rootCommand = new RootCommand("Test root command");
+    rootCommand.AddCommand(cmd);
+    var builder = new CommandLineBuilder(rootCommand).UseDefaults();
+    var parser = builder.Build();
+    TextReader inputReader = new StringReader("");
+    var outputWriter = new StringWriter();
+    var errorWriter = new StringWriter();
+    var console = new WritersConsole(inputReader, outputWriter, errorWriter);
+    var exitCode = await DafnyNewCli.ExecuteForParser(console, fullArgs, parser);
+    Assert.Equal<object>("", errorWriter.ToString());
+    Assert.Equal(0, exitCode);
+    Assert.True(callbackCalled);
+  }
+}

Source/DafnyDriver/Commands/RunCommand.cs

@@ -49,7 +49,7 @@ static RunCommand() {
       Concat(DafnyCommands.ConsoleOutputOptions).
       Concat(DafnyCommands.ResolverOptions);
 
-  public static Command Create() {
+  public static Command Create(Func<DafnyOptions, int> continuation = null) {
     var result = new Command("run", "Run the program.");
     result.AddArgument(DafnyCommands.FileArgument);
     result.AddArgument(UserProgramArguments);
@@ -63,7 +63,9 @@ public static Command Create() {
       options.Compile = true;
       options.RunAfterCompile = true;
       options.ForceCompile = options.Get(BoogieOptionBag.NoVerify);
-
+      if (continuation != null) {
+        return continuation(options);
+      }
       return await SynchronousCliCompilation.Run(options);
     });
     return result;

Source/DafnyDriver/DafnyNewCli.cs

@@ -172,6 +172,10 @@ private static void ProcessOption(InvocationContext context, Option option, Dafn
   }
 
   public static Task<int> Execute(IConsole console, IReadOnlyList<string> arguments) {
+    return ExecuteForParser(console, arguments, Parser);
+  }
+
+  public static Task<int> ExecuteForParser(IConsole console, IReadOnlyList<string> arguments, System.CommandLine.Parsing.Parser parser) {
     foreach (var symbol in AllSymbols) {
       if (symbol is Option option) {
         if (!option.Arity.Equals(ArgumentArity.ZeroOrMore) && !option.Arity.Equals(ArgumentArity.OneOrMore)) {
@@ -180,7 +184,7 @@ public static Task<int> Execute(IConsole console, IReadOnlyList<string> argument
       }
     }
 
-    return Parser.InvokeAsync(arguments.ToArray(), console);
+    return parser.InvokeAsync(arguments.ToArray(), console);
   }
 
   private static readonly MethodInfo GetValueForOptionMethod;

Source/DafnyDriver/WritersConsole.cs

@@ -5,7 +5,7 @@
 
 namespace Microsoft.Dafny;
 
-class WritersConsole : IConsole {
+public class WritersConsole : IConsole {
   public TextReader InputWriter { get; }
   public TextWriter ErrWriter { get; }
   public TextWriter OutWriter { get; }

docs/DafnyRef/UserGuide.md

@@ -2294,6 +2294,8 @@ and what information it produces about the verification process.
 
 * `--no-verify` - turns off verification (for translate, build, run commands)
 
+* `--do-boogie-translation` - turns on translation to Boogie after resolving or if `--no-verify` is set. Automatically set if `--bprint` is set.
+
 * `--verify-included-files` (was `-verifyAllModules`) - verify modules that come from include directives.
 
   By default, Dafny only verifies files explicitly listed on the command