Mycroft92 (Sep 22 2021 at 09:48): 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.
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.
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
Mycroft92 (Sep 22 2021 at 10:01):VScoq seems to have it's own zulip, I will ask there. Thanks for your response Karl.
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
Mycroft92 (Sep 22 2021 at 10:03):Thanks again. I didn't know about this.
Karl Palmskog (Sep 22 2021 at 10:06):we can move this topic to the VsCoq stream (ping @Théo Zimmermann )
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.
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.
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
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.
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
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.
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).
This topic was moved here from #Coq users > VScode prettify symbols by Théo Zimmermann
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.
Karl Palmskog (Sep 22 2021 at 18:24):I think you mean Théo Winterhalter
Paolo Giarrusso (Sep 22 2021 at 18:25):(and I'm aware of the ANSSI guidelines, but I can't change Iris).
Paolo Giarrusso (Sep 22 2021 at 18:26):whoops thanks, typo fixed
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.
Paolo Giarrusso (Sep 22 2021 at 18:29):sure, I'm not imposing my (or Robbert/Ralf's) preferences on others
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"
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
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
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
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.)
Paolo Giarrusso (Sep 22 2021 at 18:37):(You just reminded me of prettifiers for layout-sensitive languages like Haskell, Théo).
Paolo Giarrusso (Sep 22 2021 at 18:37):(Yes they exist, but we're luckier here)
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: Jun 04 2023 at 23:30 UTC