From 63e5d7f397a1a119319522784b0afd2c6679362b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Mon, 14 Aug 2023 15:47:00 -0500 Subject: [PATCH] Feat: Added the test command (#420) 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, even that testing often precedes verification. If users want still to run regular tests and run with verification, they can use the trick of "build with custom arguments" and set up their custom command, or just use the terminal. --- package.json | 15 ++++++++++++++ src/commands.ts | 1 + src/ui/compileCommands.ts | 43 +++++++++++++++++++++++++++++---------- 3 files changed, 48 insertions(+), 11 deletions(-) diff --git a/package.json b/package.json index dc3ce0a4..d2eabb3c 100644 --- a/package.json +++ b/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", @@ -267,6 +278,10 @@ "command": "dafny.buildCustomArgs", "title": "Dafny: Build with Custom Arguments" }, + { + "command": "dafny.test", + "title": "Dafny: Test" + }, { "command": "dafny.run", "title": "Dafny: Run" diff --git a/src/commands.ts b/src/commands.ts index 73d33007..3b5dafa4 100644 --- a/src/commands.ts +++ b/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'; diff --git a/src/ui/compileCommands.ts b/src/ui/compileCommands.ts index 402fb934..0be408d0 100644 --- a/src/ui/compileCommands.ts +++ b/src/ui/compileCommands.ts @@ -11,18 +11,32 @@ import { Messages } from './messages'; const OutputPathArg = '--output'; +enum CommandType { + Build, + Run, + Test +} + 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, CommandType.Build, false)), + commands.registerCommand(DafnyCommands.BuildCustomArgs, () => + buildRunOrTest(installer, CommandType.Build, true)), + commands.registerCommand(DafnyCommands.Run, () => + buildRunOrTest(installer, CommandType.Run, false)), + commands.registerCommand(DafnyCommands.Test, () => + buildRunOrTest(installer, CommandType.Test, false)) ); return new CompileCommands(); } } -async function buildOrRun(installer: DafnyInstaller, useCustomArgs: boolean, run: boolean): Promise { +// Build: run == false && test == false +// Run: run == true +// Test: run == false && test == true +async function buildRunOrTest(installer: DafnyInstaller, commandType: CommandType, useCustomArgs: boolean): Promise { const document = window.activeTextEditor?.document; if(document == null) { return false; @@ -34,7 +48,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, commandType, useCustomArgs).createCompilerCommand(); if(compilerCommand == null) { return false; } @@ -52,8 +66,8 @@ class CommandFactory { public constructor( private readonly installer: DafnyInstaller, private readonly fileName: string, - private readonly useCustomArgs: boolean, - private readonly run: boolean + private readonly commandType: CommandType, + private readonly useCustomArgs: boolean ) {} public async createCompilerCommand(): Promise { @@ -101,14 +115,21 @@ class CommandFactory { } private withCompileAndRun(args: string[]): string[] { - if(this.run) { - return [ 'run', ...args ]; + if(this.commandType === CommandType.Run) { + return [ 'run', '--no-verify', ...args ]; + } + if(this.commandType === CommandType.Test) { + return [ 'test', '--no-verify', ...args ]; + } + if(this.commandType === CommandType.Build) { + return [ 'build', ...args ]; } - return [ 'build', ...args ]; + throw new Error(`Unknown command type: ${this.commandType}`); } private withOutputPath(args: string[]): string[] { - if(this.run) { + //if(this.run || this.test) { + if(this.commandType === CommandType.Run || this.commandType === CommandType.Test) { return args; } if(args.some(arg => arg.includes(OutputPathArg))) {