-
Notifications
You must be signed in to change notification settings - Fork 19
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Some command to run the CLI verify from the IDE #383
Comments
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 ...
"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 |
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 |
while you're at it - be nice if changing dafny status (onChange, onSave, none at all) didn't require a restart; |
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.
Dafny: Verify
that will build a CLI for the current file--boogie-filter
for the current operationmeasure-complexity
or--log-format text
The text was updated successfully, but these errors were encountered: