Feat: Added the test command

Fixes #417
This PR adds the "Test" command in the contextual Dafny menu.

A bit of context. It's not possible to put several Main methods in included files, but it's definitely possible to put tests in each file as needed.
Currently, to run tests, one typically right-clicks "Dafny > build with custom arguments", and then replace everything with "test". There is not even a shortcut for that, although the "test" command is fully supported in Dafny.
Moreover, I am adding the "--no-verify" flag by default both on tests and run because
1) it's in the context of a development environment
2) The minimum required for `dafny run` and `dafnyt test` is that the program resolves and the compiler can compile it.
3) Verification of the entire file before testing is at best redundant because it was already verified in the IDE, at worst it forces the user to add a bunch of "assume false" in their code just because they haven't prove some assertions they conjectured.

I think it's fair to say that the usual workflow of testing is complementary to verification, meaning it makes it possible to experiment on specifications before proving them.

package.json

@@ -56,6 +56,11 @@
           "command": "dafny.run",
           "group": "7_Dafny@7"
         },
+        {
+          "when": "editorTextFocus && editorLangId == dafny",
+          "command": "dafny.test",
+          "group": "7_Dafny@8"
+        },
         {
           "when": "editorTextFocus && editorLangId == dafny && dafny.counterexampleMenu.CanShowCounterExample",
           "command": "dafny.showCounterexample",
@@ -86,6 +91,12 @@
         "mac": "f5",
         "when": "editorTextFocus && editorLangId == dafny"
       },
+      {
+        "command": "dafny.test",
+        "key": "shift+f5",
+        "mac": "⇧f5",
+        "when": "editorTextFocus && editorLangId == dafny"
+      },
       {
         "command": "dafny.buildCustomArgs",
         "key": "f6",
@@ -261,6 +272,10 @@
         "command": "dafny.buildCustomArgs",
         "title": "Dafny: Build with Custom Arguments"
       },
+      {
+        "command": "dafny.test",
+        "title": "Dafny: Test"
+      },
       {
         "command": "dafny.run",
         "title": "Dafny: Run"

src/commands.ts

@@ -2,6 +2,7 @@ export namespace DafnyCommands {
   export const Build = 'dafny.build';
   export const BuildCustomArgs = 'dafny.buildCustomArgs';
   export const Run = 'dafny.run';
+  export const Test = 'dafny.test';
   export const ShowCounterexample = 'dafny.showCounterexample';
   export const HideCounterexample = 'dafny.hideCounterexample';
   export const CopyCounterexamples = 'dafny.copyCounterexamples';

src/ui/compileCommands.ts

@@ -14,15 +14,23 @@ const OutputPathArg = '--output';
 export default class CompileCommands {
   public static createAndRegister(installer: DafnyInstaller): CompileCommands {
     installer.context.subscriptions.push(
-      commands.registerCommand(DafnyCommands.Build, () => buildOrRun(installer, false, false)),
-      commands.registerCommand(DafnyCommands.BuildCustomArgs, () => buildOrRun(installer, true, false)),
-      commands.registerCommand(DafnyCommands.Run, () => buildOrRun(installer, false, true))
+      commands.registerCommand(DafnyCommands.Build, () =>
+        buildRunOrTest(installer, false, false, false)),
+      commands.registerCommand(DafnyCommands.BuildCustomArgs, () =>
+        buildRunOrTest(installer, true, false, false)),
+      commands.registerCommand(DafnyCommands.Run, () =>
+        buildRunOrTest(installer, false, true, false)),
+      commands.registerCommand(DafnyCommands.Test, () =>
+        buildRunOrTest(installer, false, false, true)),
     );
     return new CompileCommands();
   }
 }
 
-async function buildOrRun(installer: DafnyInstaller, useCustomArgs: boolean, run: boolean): Promise<boolean> {
+// Build: run == false && test == false
+// Run:   run == true
+// Test:  run == false && test == true
+async function buildRunOrTest(installer: DafnyInstaller, useCustomArgs: boolean, run: boolean, test: boolean): Promise<boolean> {
   const document = window.activeTextEditor?.document;
   if(document == null) {
     return false;
@@ -34,7 +42,7 @@ async function buildOrRun(installer: DafnyInstaller, useCustomArgs: boolean, run
   if(!await document.save()) {
     return false;
   }
-  const compilerCommand = await new CommandFactory(installer, document.fileName, useCustomArgs, run).createCompilerCommand();
+  const compilerCommand = await new CommandFactory(installer, document.fileName, useCustomArgs, run, test).createCompilerCommand();
   if(compilerCommand == null) {
     return false;
   }
@@ -53,7 +61,8 @@ class CommandFactory {
     private readonly installer: DafnyInstaller,
     private readonly fileName: string,
     private readonly useCustomArgs: boolean,
-    private readonly run: boolean
+    private readonly run: boolean,
+    private readonly test: boolean
   ) {}
 
   public async createCompilerCommand(): Promise<string | undefined> {
@@ -102,13 +111,16 @@ class CommandFactory {
 
   private withCompileAndRun(args: string[]): string[] {
     if(this.run) {
-      return [ 'run', ...args ];
+      return [ 'run', '--no-verify', ...args ];
+    }
+    if(this.test) {
+      return [ 'test', '--no-verify', ...args];
     }
     return [ 'build', ...args ];
   }
 
   private withOutputPath(args: string[]): string[] {
-    if(this.run) {
+    if(this.run || this.test) {
       return args;
     }
     if(args.some(arg => arg.includes(OutputPathArg))) {