F5 in VS extension discards cached results about dafny HOT 6 CLOSED

Wouldn't it make more sense to restart verification immediately as soon as there are new changes, and not require any explicit action to cancel the verification? I've often wished the Emacs mode worked this way.

from dafny.

Sure, restarting verification immediately as soon as there are new changes sounds even better, as long as we don't throw away cached verification results when we do so.

from dafny.

I thought the Emacs mode for Dafny already does kill any ongoing verification when the buffer has been modified (whereas the Visual Studio mode does not).

from dafny.

Nope; Emacs waits for a full verification round to complete before starting another one.

The reason is mostly technical, I think: back when I wrote this code, I don't think Dafny had a nice API to interrupt an ongoing verification without loosing the partial results.

I'm not sure restarting after every modification is the best. That's going to be a lot of restarts.

What about restarting every time the file is saved?

Clément.

from dafny.

Restarting on save sounds like a good option to me.

from dafny.

Fine with me as well.

from dafny.