Inconsistent state: Can only add a comand to the current focus

[qcfu-bu]

When working with long files (over 1500 lines of code), I often encounter instances where vscoq refuses to step through the proof. Neither stepping one line at a time nor step to point works. An error message Inconsistent state: Can only add a comand to the current focus is displayed. I know that coq works correctly on my machine because proof general in emacs does not exhibit such an issue.

[fakusb]

Can you describe which kind of behaviour/usage leads to that error?

Did you use 'search/replace' or another editor feature that changed the document anywhere else than at the current cursor? Does the error persist after reloading the file? (for example via 'F1 -> reload window')

[qcfu-bu]

Now that you mention it, it might be caused by edits made by the "find replace" for search and replacing string. I also sometimes revert the file to a previous version using git.

So vscoq's internal coq process does reset its state when edits are made using these methods?

[fakusb]

In the way vscoq is currently written, vscoq itself needs to keep track where different "sentences" (command terminated with .', for example, tactics) are in the text-file, as we only want to pass changes to the content of those sentences to coq itself, but not for example whitespace changes or shifts of those sentences: You can edit a proof script while other proofs below stay 'proofchecked', although the offset of those in the document might change. This makes the asynchronous proof checking more usable.

As a trade-of, we assume that only one position, near the cursor, gets edited, so simplify the heuristic that tries to match the document locations before and after an edit.

There is a rewrite of vscoq on the way that moves that logic into coq itself, which will probably improve on this behaviour.

In the current state, we might could re-force a complete reevaluation when we encounter an error we currently report with 'Inconsistent state: Can only add a comand to the current focus'.

[qcfu-bu]

I retract my previous statement. Vscoq definitely does encounter inconsistent state error when just editing/replaying proofs normally, without me even touching git or find replace. These errors happened to me extremely often yesterday when just stepping though a file. The reload window command does reset vscoq and this error, but it breaks the workflow so isn't ideal.

I have a suspicion that it may be due to the caching or asynchronous replay. Proof general will step through a proof completely sequentially, whereas vscoq will buffer stuff and immediately allow stepping by the cursor. But I'm not familiar with vscoq's inner workings so this might not be the case.

[qcfu-bu]

I think I've found the source of why this is happening to me. I'm a user of the Vim extension for vscode. Yanking and pasting code using the vim extension causes the inconsistent state error, especially if yanking several lines worth of code.