I have a case where a step over a cbv which produces a slightly largish term (4000 lines in 80 chars display). The cbv as such takes 3 ms, but the display of the term takes 2 minutes. In CoqIDE I see two differences: first it does not block until the term is displayed and second it takes about 1s until the term is displayed, so about 100x faster. I guess this is known. Is it understood what the root cause is?
@Michael Soegtrop if you have a short example
.v file, please open a VsCoq issue. This could be relevant for the test suite that @Huỳnh Trần Khanh mentioned
Assuming this just depends on the term size, a small example should be easy to produce.
I created https://github.com/coq-community/vscoq/issues/317.
Last updated: Jan 30 2023 at 18:04 UTC