I am new to VsCoq (used and liked Coqide before but it became so slow with recent updates...).
Another unrelated issue is that at some seemingly random points the proof view uses only around 10 chars per line, even though the tab is much wider. Any idea? If this issue is not known, I can try to understand when this happens.
SearchAbout was deprecated in Coq 8.11 and has been removed in 8.12 in favor of a more powerful
Search. (So it's not related to the IDE you use.)
I see. This explains SearchAbout. Thanks.
For the other problems, you may want to report them as issues (or maybe someone has reported something similar): https://github.com/coq-community/vscoq/issues/
This topic was moved by Théo Zimmermann to #Coq users > CoqIDE slowness on macOS
@Ori Lahav I've surely seen the 10 chars per line issue, but never reported, and I agree it's pretty annoying
My weak workaround is to open another proof tab, jump back, and then things seem to work better. If I do it at the beginning of a theorem, it sticks fixed longer, or sth.
Which is still bad.
Paolo Giarrusso said:
Ori Lahav I've surely seen the 10 chars per line issue, but never reported, and I agree it's pretty annoying
He reported it here: https://github.com/coq-community/vscoq/issues/151
As I say there, zooming in and the out does fix the problem temporarily.
Last updated: Jun 04 2023 at 23:30 UTC