QuickCheck button on the editor bar

[c4rlo14]

It could be useful to have a new QuickCheck button on the editor bar, beside the POG button, which would run POG and QuickCheck immediately after.

[nickbattle]

We have to be careful with this. It seems like a natural thing to do, and when you have small test specs, which can be checked in a fraction of a second, it would probably work fine. But we have to be careful with larger specs, especially if they generate complex obligations (eg. operation POs) that QuickCheck will struggle with (or which may timeout).

The problem is that VDMJ is fundamentally single-threaded. So when you ask it to (say) typecheck the specification, it can't safely do anything else at the same time. Similarly with POG and QC.

But of course the VSCode client/server design allows asynchronous user actions, that are sent whenever the user does something. This is usually dealt with by the LSP Server itself being single threaded -- for example, when you typecheck the specification, the Server does not respond to the request until that is complete. So even if you keep editing and saving while a long spec typechecks, those requests will not overlap (I assume they are queued at the Client). A similar issue exists if you edit the spec while the interpreter is running. In that case, the next time you try to print f(123), say, the Console will tell you that the spec has changed and you should restart. Similarly, if you print f(1) while a previous execution is in progress, the Console will say, "Still running f(456)" or whatever.

However, for some GUI actions that can take a long time, we background the action at the Server and send progress updates. We do this for POG and QC. But that means that, in principle, other requests can interleave with them and cause problems.

Sometimes, these interleavings are detected and stopped. But not always -- the whole point of backgrounding an action is to allow other things to proceed. So if we cause QC to run automatically, we are increasing the likelihood of overlapping calls, because users will "click and forget". Whereas we need them to be sane and wait for things to complete.

So it may be that we need a firmer thread-control system in the Server. That's plausible. But I would not recommend automatic QuickChecking until that situation is sorted out. And that means deciding what the user will see when they are prevented from (say) editing a file because QuickCheck is still running.