Stream: math-comp users

Topic: Why doesn't math-comp use cool notation


view this post on Zulip walker (Oct 26 2022 at 09:42):

I am talking about unicode stuff, for instance membership like '∈' instead of '\in' ?

view this post on Zulip Julien Puydt (Oct 26 2022 at 09:50):

It's a good question because I see the intent (there's also something to be said about <= for $\subset$, & for $\cap$, etc) ; but the question how to type them is another: if it's readable but unwritable...

view this post on Zulip Théo Zimmermann (Oct 26 2022 at 10:02):

Nowadays, every standard IDE solution has an input method for Unicode though.

view this post on Zulip Théo Zimmermann (Oct 26 2022 at 10:02):

But this was certainly not the case when math-comp was started.

view this post on Zulip Karl Palmskog (Oct 26 2022 at 10:54):

there is a quite strong case for completely avoiding Unicode, which is that they can easily confuse people, hence why we get stuff like this in the Common Criteria eval recommendations:

Developers Rule 4.7. Notations shall favor regular ASCII characters over Unicode characters, so that they do not require a particular IDE setup to use them.

view this post on Zulip Julien Puydt (Oct 26 2022 at 11:28):

And there I have to notice that if you're to use Coq+MC to do mathematics, it's a quite strong case for being able to at least display things like it is done in mathematics!

It would definitely make sense to type \in, \subset, \cup, \cap (ie: type and save ASCII so respect rule 4.7) but have the IDE display them as \in, \cup, \cap (ie: be flesh-mathematician compatible)...

view this post on Zulip Théo Zimmermann (Oct 26 2022 at 11:38):

Yes, then this is not Unicode notation but improvement on the IDE side.

view this post on Zulip Théo Zimmermann (Oct 26 2022 at 11:38):

Company-Coq already has something like this.

view this post on Zulip Théo Zimmermann (Oct 26 2022 at 11:38):

And jsCoq has some experiments around this as well (that could be transferred to VsCoq).

view this post on Zulip Théo Zimmermann (Oct 26 2022 at 11:39):

The interesting thing about this approach is that it can allow going much beyond what linear Unicode gives us. For instance, by displaying a notation in 2D.

view this post on Zulip Julien Puydt (Oct 26 2022 at 11:54):

@Théo Zimmermann Indeed, and it's nicer.

view this post on Zulip Michael Soegtrop (Oct 26 2022 at 11:55):

One argument against fancy notations is that it might make it easier for an adversarial contributor to pass reviews for intentionally wrong stuff. One should not use a system for inspecting code for reviews which allow things like hiding code with unicode hacks. And having to look at code for reviews with a different tool / in a different format will make reviews more error prone since one is not used to the display.

view this post on Zulip Paolo Giarrusso (Oct 26 2022 at 11:58):

You definitely don't need unicode to hide things.

view this post on Zulip Théo Zimmermann (Oct 26 2022 at 12:02):

I think for making the job of reviewers nicer, people should inspire from what was done for math-comp (four-color IIRC) where everything that is needed (definition, notations) to understand the final theorem is presented in a single file. This means that you can have fancy notations in the proof and they are completely fine, as long as you limit yourself in what the reviewers need to understand.

view this post on Zulip Michael Soegtrop (Oct 26 2022 at 12:22):

Of course such a design helps for reviews of a paper on a theorem. I think it is more of a problem to avoid that something gets into the standard library or another developments which is intended to confuse readers about what they see. But of course @Paolo Giarrusso is right that there are other ways of doing this without Unicode.

view this post on Zulip walker (Oct 26 2022 at 12:34):

So it mostly preference matters, that is good to know that there are no deep hidden justifications!

view this post on Zulip walker (Oct 26 2022 at 12:37):

Théo Zimmermann said:

The interesting thing about this approach is that it can allow going much beyond what linear Unicode gives us. For instance, by displaying a notation in 2D.

is there a plugin for vscode that does that? allows me to type \in ... save it as "\in" but display it as ∈ ?

view this post on Zulip walker (Oct 26 2022 at 12:38):

I am using vscoq but the plugin I use which is called Generic Input method allows gives you shortcuts to write things like ∈ directly.

view this post on Zulip Théo Zimmermann (Oct 26 2022 at 12:44):

walker said:

Théo Zimmermann said:

The interesting thing about this approach is that it can allow going much beyond what linear Unicode gives us. For instance, by displaying a notation in 2D.

is there a plugin for vscode that does that? allows me to type \in ... save it as "\in" but display it as ∈ ?

No, I don't think that this exists at the current time.

view this post on Zulip Reynald Affeldt (Oct 26 2022 at 12:49):

Théo Zimmermann said:

Company-Coq already has something like this.

We have been using this facility in MathComp-Analyis (https://github.com/math-comp/analysis/blob/master/.dir-locals.el).

view this post on Zulip Enrico Tassi (Oct 26 2022 at 12:50):

I don't think there would be much resistance against a file with unicode notations for MC stuff to be loaded optionally. At least this is what I recall from the last time we discussed that.
At the same time I spent the last week playing with Lambdapi where you must input unicode characters and the extension they suggest does not really work as you want and in the end it was a total pain. I would have really loved to be able to write := instead it's utf8 glyph which I could not get by any combo. Nobody wants that for MC, believe me.

view this post on Zulip Pierre Roux (Oct 26 2022 at 14:18):

Théo Zimmermann said:

I think for making the job of reviewers nicer, people should inspire from what was done for math-comp (four-color IIRC) where everything that is needed (definition, notations) to understand the final theorem is presented in a single file. This means that you can have fancy notations in the proof and they are completely fine, as long as you limit yourself in what the reviewers need to understand.

I don't know for four-color but this was definitely done for odd-order: https://github.com/math-comp/odd-order/blob/master/theories/stripped_odd_order_theorem.v

view this post on Zulip Paolo Giarrusso (Oct 26 2022 at 19:11):

Pierre: yep, and also the "math-comp 4-color paper" reports the theorem can be stated "from scratch" in ~200 LoCs

view this post on Zulip Paolo Giarrusso (Oct 26 2022 at 19:12):

@Enrico Tassi indeed, one needs to align the editor config with the library. Iris ships editor configs for at least Emacs and VScode

view this post on Zulip Paolo Giarrusso (Oct 26 2022 at 19:14):

as an extra point: if people _do_ use actual unicode, unicode-on-display extensions can become inconvenient, unless the unicode and ASCII alternatives are perfectly in sync...

view this post on Zulip Enrico Tassi (Oct 26 2022 at 19:56):

But are there notation with no "pure ASCII" counterparts? This is what I object against. E.g. the day you have to use CoqIDE and Iris, are you dead/alone?

view this post on Zulip Paolo Giarrusso (Oct 26 2022 at 20:32):

IIRC, Robbert Krebbers uses CoqIDE on Linux and some Linux input method for this

view this post on Zulip Paolo Giarrusso (Oct 26 2022 at 20:32):

and yes, I have colleagues with the same objections

view this post on Zulip walker (Oct 26 2022 at 23:24):

well, I am not as expert as you guys, but I know that there is usually a principle for designing APIs/languages that says:
there should be ideally one way to do a given task, and at minimum there should be just one good way where every other way is bad practice.

Now having both unicode + ascii notations sounds like two good ways for doing the same thing, that would invite new users like myself to have the most artistic mixing of both notations. :sweat_smile:

view this post on Zulip Paolo Giarrusso (Oct 27 2022 at 04:51):

I don't think such rules are so universal, even if that's certainly Python's motto

view this post on Zulip Paolo Giarrusso (Oct 27 2022 at 04:57):

and compared to all the other scenarios where Coq has multiple ways to do the same thing (stdlib vs stdpp vs math-comp vs other libraries), this seems the least harmful

view this post on Zulip Enrico Tassi (Oct 27 2022 at 06:38):

The reule does not apply here. It is more like having a remote control for opening your car, but also the good old key. Im objecting not having the key, since it has way less chances of failing a user, but I'd use the remote all the times.

view this post on Zulip Enrico Tassi (Oct 27 2022 at 06:40):

It is more about stratification of APIs. At each layer you rule can apply, I guess.

view this post on Zulip Théo Zimmermann (Oct 27 2022 at 06:49):

FWIW CoqIDE already has its own internal Unicode input method.

view this post on Zulip Julien Puydt (Oct 27 2022 at 06:52):

Oh? I'm using CoqIDE and I don't know about it...

view this post on Zulip Théo Zimmermann (Oct 27 2022 at 06:53):

https://coq.inria.fr/refman/practical-tools/coqide.html#coqide-unicode

view this post on Zulip Julien Puydt (Oct 27 2022 at 06:59):

I should read that at one point...

view this post on Zulip Julien Puydt (Oct 27 2022 at 07:07):

(perhaps it also explains why I need to quit & reopen anytime I change the file structure of my pet project)

view this post on Zulip walker (Oct 27 2022 at 12:45):

Paolo Giarrusso said:

I don't think such rules are so universal, even if that's certainly Python's motto

I didn't know that this was python principle, But I read it at some point an old document from 80s/90s about how to design a language, maybe that is what also inspired python, But I think that it is a good guieline (Look at C++ for the extreme case of the opossite of that principle)

view this post on Zulip Paolo Giarrusso (Oct 27 2022 at 23:07):

It's definitely a factor; but most of the arguments apply less or not at all. You can combine code using different notations if desired, the obstacle to communication is smaller, etc etc.
In contrast, the presence of canonical structures + typeclasses + modules has real problems: they achieve similar goals but in different and incompatible ways, and some features support only one or only the other


Last updated: Feb 02 2023 at 13:03 UTC