Add Semi-Continuous mode for larger and slower files

[tlsomers]

This PR adds a 'SemiContinuous' mode as a compromise between continually checking in the background, but skipping proofs in the foreground.

Using this mode, the proof state at the cursor can be determined more quickly, as prior proofs are skipped. However, the continuous checker is still run in the background to continually check all proofs in the file.

Additionally, a new NonOpaqueProof task is added for proofs which are not opaque and cannot be delegated, but can still be skipped using the Skip option or in SemiContinuous mode.

Even using SemiContinuous mode, changing the cursor position may be slow as LSP commands are currently run at 1 byte per loop (hence 1 byte per background Coq command). The following SEL pull request allows LSP commands to be read in one iteration:
gares/sel#10

[gares]

I like the idea, but:

Additionally, a new NonOpaqueProof task is added for proofs which are not opaque and cannot be delegated, but can still be skipped using the Skip option or in SemiContinuous mode.

This seems wrong to me. A piece of Coq code like

Definition foo : nat.
Proof. exact 3. Defined.

Cannot be skipped or processed in the background without potentially generating spurious failures.
Even if its syntax is akin a proof block, it really means Definition n : nat := 3. and the definition just after it can fail to typecheck if the value of n is not 3, eg Definition v : Vector.t bool n := vcons .. vcons .. vcons .. vnil. So I'm afraid that part of the PR needs to be changed.

[rtetley]

Hey @tlsomers ! What is the status on this ? Would you willing to make the change so we can merge ?