Michael Soegtrop (Nov 23 2022 at 10:22): Michael Soegtrop (Nov 23 2022 at 10:22):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?
Karl Palmskog (Nov 23 2022 at 12:03):@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
Michael Soegtrop (Nov 23 2022 at 12:16):Assuming this just depends on the term size, a small example should be easy to produce.
Michael Soegtrop (Nov 23 2022 at 12:38):I created https://github.com/coq-community/vscoq/issues/317.
Last updated: Jun 04 2023 at 23:30 UTC