vio2vo background compilation stops on failure in current file

[RalfJung]

Steps to reproduce

• Open some file in quick+vio2vo mode, hit C-c C-b

Expected behavior

Background compilation of vio2vo goes on until nothing is left to do or there is a failure (and, in case "Keep Going" is enabled, until all files that are left to do fail).

Actual behavior

If there is a failure in the top-level file that I am editing, vio2vo stops. I don't understand how that's useful behavior, it means vio2vo will not very often do jobs in background for me -- typically, when I write proof scripts of do refactoring, I do have failures all the time and make progress by fixing them, not by writing flawless code that compiles on the first attempt.

[hendriktews]

Ralf Jung notifications@github.com writes:

If there is a failure in the top-level file that I am editing, vio2vo stops. I don't understand how that's useful behavior, it means vio2vo

I agree that this could be improved. However, as far as I know, the Proof General error handling does not really distinguish whether the user hit C-c C-c or whether Coq choked on something. In the first case you definitely want all background stuff to stop, therefore, you also get it in the second case.

The problem are all the tricky corner cases. Assume you have

Require A.
Some command with an error.
Require B.

When Coq delivers the error for the second command, the compilation for B might still be going on. The error causes Require B to be removed from the queue region, therefore all the ancestors of B should be unlocked. Therefore I decided to kill the compilation of B. Unfortunately, this also kills all scheduled vio2vo for A, kind of as collateral damage...

[RalfJung]

I understand. Of course things are never as simple as they seem.