Stream: VsCoq devs & users

Topic: Prettification vs. Unicode symbols


view this post on Zulip Clément Pit-Claudel (Sep 24 2021 at 16:00):

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

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 ^^)

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

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

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

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

view this post on Zulip Paolo Giarrusso (Sep 24 2021 at 21:11):

I really miss the ease of indenting statement-oriended languages...

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

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

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

view this post on Zulip Karl Palmskog (Sep 27 2021 at 09:29):

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

view this post on Zulip Pierre-Marie Pédrot (Sep 27 2021 at 09:30):

c'mon it's 2021 now, how a desktop client can fail at printing unicode?

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

view this post on Zulip Karl Palmskog (Sep 27 2021 at 09:33):

Alectryon broke down on Unicode Coq files for us before this patch: https://github.com/cpitclaudel/alectryon/commit/febf8310e1eb4954fb1dd4815aa3f5d91230627e

Probably there lots of similar issues out there in various tools.

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

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

view this post on Zulip Karl Palmskog (Sep 27 2021 at 09:59):

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

view this post on Zulip Karl Palmskog (Sep 27 2021 at 10:03):

These don't look like to emojis to me, and were added in 13.0:
https://blog.emojipedia.org/content/images/2020/03/legacy-computing-symbols-unicode-13.png

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

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

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

view this post on Zulip Pierre Courtieu (Oct 01 2021 at 13:13):

In 2021 switching to non monospace font still break indentation…

view this post on Zulip Paolo Giarrusso (Oct 01 2021 at 21:57):

but that’s what monospace unicode fonts are for :-)

view this post on Zulip Clément Pit-Claudel (Oct 04 2021 at 00:25):

https://github.com/cpitclaudel/monospacifier
Paolo Giarrusso said:

but that’s what monospace unicode fonts are for :-)

All fonts are monospace if you look at them sternly enough https://github.com/cpitclaudel/monospacifier

view this post on Zulip Clément Pit-Claudel (Oct 04 2021 at 00:26):

Pierre-Marie Pédrot said:

c'mon it's 2021 now, how a desktop client can fail at printing unicode?

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

view this post on Zulip Clément Pit-Claudel (Oct 04 2021 at 00:32):

Paolo Giarrusso said:

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)?

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)

view this post on Zulip Gaëtan Gilbert (Oct 04 2021 at 08:17):

I don't like indentation-to-align in general, that code should be indented as

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

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

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


Last updated: Jan 30 2023 at 18:04 UTC