Stream: VsCoq devs & users

Topic: Vscoq vs coqide and the STM


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Sep 01 2020 at 22:48):

Hm, I see!


Last updated: Jan 30 2023 at 18:04 UTC