VsCoq has often “STM” problems with async proofs, but I’ve heard that coqide has no such problems. Is this covered by the known issues/ongoing work?
Things did get better a while ago, after the move to coq-community, but the problems aren’t quite fixed yet.
I’ve even heard claims that vim’s coqtail has no such problem but supports async proofs, which sounds very interesting (since I grew up as a vim user)
Coqtail is asynchronous in the sense that the editor is not locked up whle Coq is thinking (you can move the cursor, change buffers, etc), but it doesn't currently support Coq's asynchronous proof checking
Hm, I see!
Last updated: Jun 04 2023 at 23:30 UTC