Stream: VsCoq devs & users

Topic: `Stm.add called for a different state than the tip'


view this post on Zulip Yannick Forster (Jun 30 2022 at 09:40):

I now very often get the error message

Stm.add called for a different state (406) than the tip: 712.
This is not supported yet, sorry.
Not in proof mode.

when processing a buffer in parallel, finding an error in a proof. fixing the error, and then again process the file in parallel. The error occurs on the Qed. of the fixed proof, and can be fixed by stepping over the Qed with "process command" rather than "process buffer". Anybody else getting this? I don't remember seeing it before 8.16, so maybe there was a change which is not fully compatible with VsCoq

view this post on Zulip Paolo Giarrusso (Jun 30 2022 at 17:00):

It's strange you never got it before, IME

view this post on Zulip Paolo Giarrusso (Jun 30 2022 at 17:02):

my rough understanding is "the STM has rough edges, and vscoq uses it less well than coqide"; I know people plan to get rid of the STM anyway

view this post on Zulip Paolo Giarrusso (Jun 30 2022 at 17:02):

@Enrico Tassi mentioned that again recently

view this post on Zulip Enrico Tassi (Jun 30 2022 at 20:15):

I do, before the fall

view this post on Zulip Mukesh Tiwari (Aug 30 2022 at 09:52):

Interestingly, I also got this error for the time https://gist.github.com/mukeshtiwari/d23451967f7e594bbc52b878f343afb8.


Last updated: Jan 30 2023 at 18:04 UTC