Prettification vs. Unicode symbols · VsCoq devs & users

Can you expand on this? I find it to be a feature of prettifiers that they can be used inconsistently by different developers: they allow you to get your favorite display without polluting your coworkers code with your own preferences.

The problem I see with using unicode is that it means everyone in the project needs a setup that supports inputting symbols, adequate fonts to display them, …and a way to look symbols up!

This is fine if you're using an advanced text editor, or if everyone in the project agrees on a common setup, but otherwise it doesn't work so well in my experience.

Btw, does the vscode extension you use to input symbols support reverse lookups? That is, if you see ⫥ ⌲ 𝕎 in a Coq program, do you have an easy way to know how to input these? My experience is that most people don't have that setup, and as a result using unicode means your collaborators copy paste stuff around (that's why I made company-coq display tips on how to input stuff: it will tell you to type \DashV, \conictaper, and \BbbW for these — but not everyone runs Emacs + company-coq, so it's not safe to assume everyone will know how to type these.)

(FWIW, I probably bear some guilt here, since the prettify extension of vscode was modeled after the prettification feature in company-coq, so I'd like to understand what's wrong with the approach ^^)

Théo Winterhalter (Sep 24 2021 at 16:15):

No I don't have the reverse search. That is clearly a nice feature of company-coq!
I used company-coq a lot, but then lines aren't simply the same length depending on which prettifying you do, so indentation, line-breaking habits will differ (they do already differ from person to person, that's for sure).
And some people use prettifiers in combination with unicode and then you end up with something clunky like

∀ x, exists y, x = 0 → y = 1 -> False

Théo Winterhalter (Sep 24 2021 at 16:17):

And then there is the problem that sometimes, something will be displayed as θ for instance, but as theta0 when θ₀ is what you want.

Théo Winterhalter (Sep 24 2021 at 16:19):

But please forget my point about it being "evil", I should not have said that. And I don't think you should feel guilty of anything, especially not making company-coq which made life with emacs slightly more bearable.

Paolo Giarrusso (Sep 24 2021 at 21:10):

So the problem with line length is arguably a problem that prettifiers aren't projectional editors? Or more modestly that nobody yet achieved a decent Coq autointender (just like for Haskell)?

Paolo Giarrusso (Sep 24 2021 at 21:11):

Théo Zimmermann (Sep 25 2021 at 07:38):

FWIW, I was also once told that Unicode characters seriously hinder accessibility (to blind people) so individually-configured prettification can be better for that reason too.

Meven Lennon-Bertrand (Sep 27 2021 at 06:54):

Regarding the vscode extension I am using for unicode input (latex-input), there is no reverse lookup in the editor, but the correspondance table between latex codes and unicode symbols can be easily browsed/edited (so that you could add a missing symbol with your chosen shortcut). Not perfect, I admit, but that’s that

Yannick Forster (Sep 27 2021 at 09:28):

To make a case for prettifiers over unicode, this is how the Zulip desktop client displays Clément's message for me: image.png

Karl Palmskog (Sep 27 2021 at 09:29):

this is a good illustration of the argument in the Common Criteria recommendation document...

Pierre-Marie Pédrot (Sep 27 2021 at 09:30):

Pierre-Marie Pédrot (Sep 27 2021 at 09:31):

this discussion looks like it's from the 90's when people were struggling with different 8-bit ISO encodings

Karl Palmskog (Sep 27 2021 at 09:33):

Yannick Forster (Sep 27 2021 at 09:39):

I agree that it's ridiculous. It would be great if we could ensure that the Coq ecosystem with it's IDEs is stable w.r.t. such annoying things

Karl Palmskog (Sep 27 2021 at 09:48):

my understanding is that desktops are almost never up to date with the latest unicode symbols, maybe because they seem to add new ones every month

Karl Palmskog (Sep 27 2021 at 09:59):

Pierre-Marie Pédrot (Sep 27 2021 at 10:02):

I agree that anybody using emojis (in particular with modifiers) in a Coq development ought to be copiously whipped with an ultrafilter, but there is still a gap with combiner-free math symbols...

Karl Palmskog (Sep 27 2021 at 10:03):

Karl Palmskog (Sep 27 2021 at 10:06):

probably we need tools to certify that only codepoints compatible with a certain Unicode version are used in a Coq project

Pierre-Marie Pédrot (Sep 27 2021 at 10:08):

Rule of thumb: if your development seems to embody the "Hello, I would like ∃∭℘ℝ apples please. They have played us for absolute fools" meme, you're probably doing it wrong. But we shouldn't throw the baby with the bathwater...

Karl Palmskog (Sep 27 2021 at 10:20):

email led to trillions of spam, encoding standards led to hundreds of thousands of emojis. Based on those facts alone, I think it's hard to argue any technical problem should be solved due to it being the current year...

Pierre Courtieu (Oct 01 2021 at 13:13):

Paolo Giarrusso (Oct 01 2021 at 21:57):

Clément Pit-Claudel (Oct 04 2021 at 00:25):

Clément Pit-Claudel (Oct 04 2021 at 00:26):

Oh, it's not failing at displaying unicode: @Yannick Forster just doesn't have a font that knows these symbols.

Clément Pit-Claudel (Oct 04 2021 at 00:32):

Yes to projectional editing, no to auto-indenting. Basically the problem is how to indent this code, on disk:

Ltac t :=
  match goal with
  | [ H: forall x, True |- _ ] => idtac;
                                  idtac
  end.

As I've shown here it looks good without prettification, but bad with prettification:

Ltac t ≜
  match goal with
  | [ H: ∀ x, ⊤ ⊢ _ ] ⇒ idtac;
                                  idtac
  end.

A really smart IDE would display prettified code as indented without changing the on-disk indentation, but that's really hard to do properly. Especially if the starting point isn't correctly indented to begin with…

(This isn't specific to prettification, btw: you have a similar problem with indentation and non-monospace fonts)

Gaëtan Gilbert (Oct 04 2021 at 08:17):

Ltac t :=
  match goal with
  | [ H: forall x, True |- _ ] => idtac;
    idtac
  end.

Paolo Giarrusso (Oct 04 2021 at 08:22):

I use indentation-to-align sometimes, but I don’t like indentation to fight with AST structure, so I don’t think either is acceptable:

Ltac t :=
  match goal with
  | [ H: forall x, True |- _ ] => (* a line break is required unless a one-liner follows *)
    idtac; (* I wouldn’t actually break the line here, but *)
      idtac
  end.

Enrico Tassi (Oct 04 2021 at 08:26):

indentation-to-align makes sense for computer generated code. If it is code you write by yourself, then you are just looking for noise in your diffs (re-indent many lines, even if you change only one).

Indeed I could understand how non-monospace fonts could break my indentation (other than shifting things to the left, since space is usually smaller in non-monospace).

Stream: VsCoq devs & users

Topic: Prettification vs. Unicode symbols

Clément Pit-Claudel (Sep 24 2021 at 16:00):