Stream: VsCoq devs & users

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

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

Paolo Giarrusso (Jun 30 2022 at 17:00):

It's strange you never got it before, IME

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

Paolo Giarrusso (Jun 30 2022 at 17:02):

@Enrico Tassi mentioned that again recently

Enrico Tassi (Jun 30 2022 at 20:15):

I do, before the fall

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: Jun 04 2023 at 23:30 UTC