Stream: VsCoq devs & users

Topic: VScode prettify symbols


view this post on Zulip Mycroft92 (Sep 22 2021 at 09:48):

Does anyone use vscoq and prettify symbols extension? It keeps breaking on my end arbitrarily with random symbols appearing on screen. The project on github seems to be abandoned.

view this post on Zulip Karl Palmskog (Sep 22 2021 at 09:50):

are you looking at this one: https://github.com/coq-community/vscoq

Last commit was 3 months ago, which by the standards of GitHub at least would not be classified as abandoned.

view this post on Zulip Mycroft92 (Sep 22 2021 at 09:57):

VScoq version is working fine, it's the prettify-symbols extension in the description that doesn't work. https://github.com/siegebell/vsc-prettify-symbols-mode

view this post on Zulip Mycroft92 (Sep 22 2021 at 10:01):

VScoq seems to have it's own zulip, I will ask there. Thanks for your response Karl.

view this post on Zulip Karl Palmskog (Sep 22 2021 at 10:01):

yeah that project is likely abandoned. Community members might consider a fork in coq-community, as was done for the original vscoq: https://github.com/coq-community/manifesto/issues/72

See the process here: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md#proposing-a-new-package

view this post on Zulip Mycroft92 (Sep 22 2021 at 10:03):

Thanks again. I didn't know about this.

view this post on Zulip Karl Palmskog (Sep 22 2021 at 10:06):

we can move this topic to the VsCoq stream (ping @Théo Zimmermann )

view this post on Zulip Théo Winterhalter (Sep 22 2021 at 10:06):

Also Coq supports unicode with the Utf8 module so it's not that necessary to use a prettifier which will always prettify wrong things.

view this post on Zulip Mycroft92 (Sep 22 2021 at 10:07):

Hi,
The description of vscoq reads that it supports prettify-symbols extension hence I am posting this here. The extension keeps breaking on my end arbitrarily with random symbols appearing on screen. The project on github seems to be abandoned. Is there any workaround for it? Or is there a different alternative.

view this post on Zulip Karl Palmskog (Sep 22 2021 at 10:08):

many people strongly prefer having their sources as ASCII. The recommendations for using Coq in Common Criteria evaluations specifically advises against using UTF8

view this post on Zulip Mycroft92 (Sep 22 2021 at 10:13):

I personally think it reads cleaner when you are looking at say code like this: Screenshot-2021-09-22-at-3.40.38-PM.png
If only it worked well enough and played nice with syntax highlights too.

view this post on Zulip Yannick Zakowski (Sep 22 2021 at 10:48):

Fwiw I observe the same behaviour but do not know of a work around. I opened an issue about it some time ago: https://github.com/coq-community/vscoq/issues/229

view this post on Zulip Théo Winterhalter (Sep 22 2021 at 11:12):

Karl Palmskog said:

many people strongly prefer having their sources as ASCII. The recommendations for using Coq in Common Criteria evaluations specifically advises against using UTF8

That's really sad. Prettifiers are evil, especially when inconsistently used among developers of the same project. Thanks for the information though.

view this post on Zulip Théo Winterhalter (Sep 22 2021 at 11:14):

Mycroft92 said:

I personally think it reads cleaner when you are looking at say code like this: Screenshot-2021-09-22-at-3.40.38-PM.png
If only it worked well enough and played nice with syntax highlights too.

With unicode input you could still write:

From Coq Require Import Utf8.

Theorem foo :
   P Q R : Prop,
    P  (Q  R) 
    (P  Q)  (P  R).

view this post on Zulip Notification Bot (Sep 22 2021 at 11:53):

This topic was moved here from #Coq users > VScode prettify symbols by Théo Zimmermann

view this post on Zulip Paolo Giarrusso (Sep 22 2021 at 18:23):

I agree with @Théo Winterhalter . I use libraries (Iris) that (1) forbid ASCII alternatives for existing Unicode syntax (2) mostly provide Unicode-only syntax. Accordingly, prettifiers are the first thing I disable in editors that enable them by default.

view this post on Zulip Karl Palmskog (Sep 22 2021 at 18:24):

I think you mean Théo Winterhalter

view this post on Zulip Paolo Giarrusso (Sep 22 2021 at 18:25):

(and I'm aware of the ANSSI guidelines, but I can't change Iris).

view this post on Zulip Paolo Giarrusso (Sep 22 2021 at 18:26):

whoops thanks, typo fixed

view this post on Zulip Karl Palmskog (Sep 22 2021 at 18:28):

for the record, all core MathComp files are ASCII. Clearly, there is a divide in the community.

view this post on Zulip Paolo Giarrusso (Sep 22 2021 at 18:29):

sure, I'm not imposing my (or Robbert/Ralf's) preferences on others

view this post on Zulip Karl Palmskog (Sep 22 2021 at 18:31):

was more concerned here about the implication "X is the consensus" from claims of "not X is evil"

view this post on Zulip Paolo Giarrusso (Sep 22 2021 at 18:32):

@Mycroft92 anyway, that extension _is_ abandoned, so the options are either using Unicode yourself, using prettifiers in Emacs, or getting somebody to volunteer fixing that (not the original author). Or maybe some fork is more up-to-date? https://github.com/siegebell/vsc-prettify-symbols-mode/network/members

view this post on Zulip Karl Palmskog (Sep 22 2021 at 18:34):

my suggestion is to propose to fork the project (vcs-prettify-symbols-mode) in coq-community. The proposer in no way has to commit to being the maintainer, we will simply mark it as "looking for maintainer": https://github.com/coq-community/manifesto/issues/new?assignees=&labels=move-project&template=1-move-a-project.md&title=Proposal+to+move+project+X+to+coq-community

view this post on Zulip Paolo Giarrusso (Sep 22 2021 at 18:34):

https://github.com/siegebell/vsc-prettify-symbols-mode/network might help, and https://github.com/silver-dragon/vsc-prettify-symbols-mode and https://github.com/Pancaek/vsc-conceal seem to have more progress

view this post on Zulip Théo Winterhalter (Sep 22 2021 at 18:35):

Karl Palmskog said:

was more concerned here about the implication "X is the consensus" from claims of "not X is evil"

Sorry, I should have worded my claim differently. I think prettifiers are hard to make robust and can be painful at times (indentation is not the same depending on whether you use one etc.)

view this post on Zulip Paolo Giarrusso (Sep 22 2021 at 18:37):

(You just reminded me of prettifiers for layout-sensitive languages like Haskell, Théo).

view this post on Zulip Paolo Giarrusso (Sep 22 2021 at 18:37):

(Yes they exist, but we're luckier here)

view this post on Zulip Mycroft92 (Sep 22 2021 at 19:20):

Thanks for the suggestions, I think I will go with the unicode alternative instead. I will however file for the prettifier to be adopted by the community.


Last updated: Jan 30 2023 at 17:03 UTC