Stream: VsCoq devs & users

Topic: Search/SearchAbout


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

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

view this post on Zulip Ori Lahav (Jul 29 2020 at 08:55):

I see. This explains SearchAbout. Thanks.

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

view this post on Zulip Notification Bot (Jul 29 2020 at 10:56):

This topic was moved by Théo Zimmermann to #Coq users > CoqIDE slowness on macOS

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

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

view this post on Zulip Paolo Giarrusso (Aug 01 2020 at 17:26):

Which is still bad.

view this post on Zulip 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: Jan 30 2023 at 17:03 UTC