Stream: VsCoq devs & users

Topic: Term display about 100x slower than in CoqIDE


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Michael Soegtrop (Nov 23 2022 at 12:16):

Assuming this just depends on the term size, a small example should be easy to produce.

view this post on Zulip Michael Soegtrop (Nov 23 2022 at 12:38):

I created https://github.com/coq-community/vscoq/issues/317.


Last updated: Jan 30 2023 at 18:04 UTC