Skip to content

Commit

Permalink
Feat: Added the test command (#420)
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
MikaelMayer authored Aug 14, 2023
1 parent 176ed57 commit 63e5d7f
Show file tree
Hide file tree
Showing 3 changed files with 48 additions and 11 deletions.
15 changes: 15 additions & 0 deletions package.json
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down Expand Up @@ -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",
Expand Down Expand Up @@ -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"
Expand Down
1 change: 1 addition & 0 deletions src/commands.ts
Original file line number Diff line number Diff line change
Expand Up @@ -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';
Expand Down
43 changes: 32 additions & 11 deletions src/ui/compileCommands.ts
Original file line number Diff line number Diff line change
Expand Up @@ -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<boolean> {
// Build: run == false && test == false
// Run: run == true
// Test: run == false && test == true
async function buildRunOrTest(installer: DafnyInstaller, commandType: CommandType, useCustomArgs: boolean): Promise<boolean> {
const document = window.activeTextEditor?.document;
if(document == null) {
return false;
Expand All @@ -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;
}
Expand All @@ -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<string | undefined> {
Expand Down Expand Up @@ -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))) {
Expand Down

0 comments on commit 63e5d7f

Please sign in to comment.