Ori Lahav (Jul 29 2020 at 05:45): Ori Lahav (Jul 29 2020 at 05:45):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.
Karl Palmskog (Jul 29 2020 at 08:08):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.)
Ori Lahav (Jul 29 2020 at 08:55):I see. This explains SearchAbout. Thanks.
Karl Palmskog (Jul 29 2020 at 09:04):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/
Notification Bot (Jul 29 2020 at 10:56):This topic was moved by Théo Zimmermann to #Coq users > CoqIDE slowness on macOS
Paolo Giarrusso (Aug 01 2020 at 17:24):@Ori Lahav I've surely seen the 10 chars per line issue, but never reported, and I agree it's pretty annoying
Paolo Giarrusso (Aug 01 2020 at 17:26):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.
Paolo Giarrusso (Aug 01 2020 at 17:26):Which is still bad.
Théo Winterhalter (Aug 01 2020 at 17:43):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