Paolo Giarrusso (Sep 01 2020 at 19:17): Paolo Giarrusso (Sep 01 2020 at 19:17):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?
Paolo Giarrusso (Sep 01 2020 at 19:18):Things did get better a while ago, after the move to coq-community, but the problems aren’t quite fixed yet.
Paolo Giarrusso (Sep 01 2020 at 19:19):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)
Wolf Honore (Sep 01 2020 at 19:29):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
Paolo Giarrusso (Sep 01 2020 at 22:48):Hm, I see!
Last updated: Apr 20 2024 at 00:02 UTC