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
It's strange you never got it before, IME
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
@Enrico Tassi mentioned that again recently
I do, before the fall
Interestingly, I also got this error for the time https://gist.github.com/mukeshtiwari/d23451967f7e594bbc52b878f343afb8.
Last updated: Jun 04 2023 at 23:30 UTC