feature request: scope interactive verification, akin to /proc: on the command-line

[0xabu]

I'm working on a large project, with lots of included files and lots of moving parts. When I'm working on a single lemma, I often find I'm more productive by running Dafny on the command line with a suitable /proc: parameter to restrict verification to just the lemma I'm working on, rather than using the flycheck mode. It would be really nice if there was an equivalent to /proc in the Emacs mode, so I could say "just verify this lemma as I work on it, and ignore everything else".

BTW, I guess in theory that DafnyServer's caching should obviate the need for this, but it doesn't because:

• looking up the cache for all the other verification targets still has some non-zero cost, as I can observe in the flycheck progress bar
• the cache is invalidated far too frequently, causing it to go and laboriously reverify the world
• if I change a dependency like part of the spec to try to debug my lemma, I don't want it to go and reverify the world right then and there

[cpitclaudel]

Hi there,

Thanks for the detailed request and explanations. It should be quite feasible, though I wonder what a good UI for this would be. One question that might help brainstorm it:

• Do you always want to verify either one or all functions? Or do you sometimes want two/three functions together? Presumably a single one, right?

Clément.

[0xabu]

Personally, I'd be happy with a dual of /proc where I can simply type in a pattern. Assuming you want to build something higher-level above that, then yes in my usage it is always a single function/method/lemma at a time, but it would still be nice to keep the raw power of the filter expression available. I guess the ideal goal would be to identify the name of the current function from the cursor location and then verify that, but I don't know if you have all the machinery to enable it (it seems non-trivial to me!).

Thanks for considering this! Andrew

[cpitclaudel]

Maybe the filter is the simplest thing. Given my limited time, a prototype working with just a filter would probably be a good start.

I need to look at the server code and protocol definition to see if they can support this without an extension. IIRC the protocol already supports passing extra arguments.