Some command to run the CLI verify from the IDE

[seebees]

Sometimes I still need to drop back tot he CLI. I used to be able to adjust the command to have a Dafny: Verify.

I would like a way to have few flavors.

1. Dafny: Verify that will build a CLI for the current file
2. add --boogie-filter for the current operation
3. either measure-complexity or --log-format text

[robin-aws]

Independently of whether this is worth adding to the extension itself, I've just had some good success defining some custom commands for this using the Command Runner extension: https://marketplace.visualstudio.com/items?itemName=edonet.vscode-command-runner&ssr=false#overview

For example, I added this to my settings.json:

    ...
    "command-runner.terminal.name": "runCommand",
    "command-runner.terminal.autoClear": true,
    "command-runner.terminal.autoFocus": true,
    "command-runner.commands": {
        "dafny verify with filter": "dafny verify ${relativeFile} ${config:dafny.runArgs} --log-format:text --boogie-filter \"*${selectedText}*\"",
    }
}

Select the name of the function/method/lemma/etc. you want to focus on, hit Ctrl+Shift+R and select the custom command.

Season to taste for various use cases. I'd recommend including ${config:dafny.runArgs} so that you pick up options like --function-syntax:3 or --unicode-char:false. You could also make this more robust by invoking ${config:dafny.cliPath} if you have that configured rather than just dafny and assuming it's on your PATH.

[keyboardDrummer]

I think the current features that invoke the Dafny CLI from the VSCode extension should be revamped to use the VSCode tasks API, which will allow users to define common Dafny CLI invocations in a tasks.json file, and for the Dafny VSCode extension to populate this file with defaults.

[kjx]

while you're at it - be nice if changing dafny status (onChange, onSave, none at all) didn't require a restart; that "resolve" and perhpas 'audit' were also options; and that there were commands to invoke each one of those modes as a "one-off" from the CLI in the IDE...