Allow to customize parameters passed to verify in DafnyServer

[ssaavedra]

It would be great to be able to configure at the editor's settings.json the parameters that are passed to DafnyServer on verify.

Currently this is implemented on server/backend/dafny/dafnyServer.js as:

    sendVerificationRequest(request) {
        if (request.verb === stringRessources_1.DafnyVerbs.CounterExample || request.verb === stringRessources_1.DafnyVerbs.Verify) {
            this.statusbar.changeServerStatus(stringRessources_1.StatusString.Verifying);
        }
        const task = {
            args: [],
            filename: vscode_uri_1.default.parse(request.document.uri).fsPath,
            source: request.source,
            sourceIsFile: false,
        };

I'm manually changing on the extension code the args: [], in my case to add args: ['/vcsLoad:1'], but it would be great if that was exported to be user-configurable.

[fabianhauser]

Hi @ssaavedra

That sounds like a great addition. Would you mind opening a pull request for that? 🙂

Adding the setting should be possible by extending the Dafny Settings Interface and adding it to the package.json of the client part.

[ssaavedra]

Thanks for the cue, I just opened #42 😉

I have no idea about VSCode extensions (I've using the editor for a couple of hours, have been using Emacs and still doing so), so please feel free to review any issues.

Also, it seems that configuration changes are not picked up automatically by the extension and that it instead needs to be reloaded (by means of > Reload window). I suppose that is a different issue regarding the onDidChangeConfiguration event (from what I has just been reading).

[ssaavedra]

Since you just opened #43 which is the only remaining question here (now that #42 is merged), I think this issue can be now closed :)

[fabianhauser]

Great, thanks for your contribution! Your changes are included in the newest release (v0.16.0) which should be public in a couple of minutes 😊

I opened a new issue #43 to address the configuration reloading (seems that it was not properly implemented all along...)