## Stream: Coq Hackathon and Working Group, Winter 2022

### Topic: Print Notation command

#### Ana de Almeida Borges (Feb 15 2022 at 09:42):

I would like to work on https://github.com/coq/coq/issues/14907, except I don't have any idea where to start. Is there anyone who would like to join and guide me?

#### Ali Caglayan (Feb 15 2022 at 09:44):

I would be happy to help

#### Emilio Jesús Gallego Arias (Feb 15 2022 at 09:44):

I can also too Ana

#### Emilio Jesús Gallego Arias (Feb 15 2022 at 09:44):

maybe that would be a good topic

#### Emilio Jesús Gallego Arias (Feb 15 2022 at 09:45):

I need 10 minutes and I join you folks

#### Ana de Almeida Borges (Feb 15 2022 at 11:07):

@Rodrigo Raya Ali and I are back in Room 1, if you'd like to join

#### Ana de Almeida Borges (Feb 15 2022 at 13:06):

https://github.com/coq/coq/pull/15683

#### Ana de Almeida Borges (Feb 15 2022 at 14:14):

`"+"` can mean many different things, but `Print` picks one (see below). How does it pick, and is there a way to make it pick one of the others?

``````Print "+".
(*
fix add (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| S p => S (add p m)
end
: nat -> nat -> nat

*)
``````

#### Janno (Feb 15 2022 at 14:16):

I am guessing but it might be that it picks the one listed as "default interpretation" in `Locate "+"`. If not then that's probably a bug.

#### Ana de Almeida Borges (Feb 15 2022 at 14:23):

So, `"+"` doesn't mean anything. There is a process translating `"+"` to the notation key `"_ + _"`. With `Locate "_ + _"` we obtain:

``````Notation "x + y" := (Nat.add x y) : nat_scope (default interpretation)
Notation "x + y" := (sum x y) : type_scope
``````

and indeed `Nat.add` is the default one. So this makes sense.

However, `Locate "+"` includes other options, many of which are default:

``````Notation "{ A } + { B }" := (sumbool A B) : type_scope
(default interpretation)
Notation "A + { B }" := (sumor A B) : type_scope (default interpretation)
Notation "x + y" := (Nat.add x y) : nat_scope (default interpretation)
Notation "x + y" := (sum x y) : type_scope
``````

I suppose the translation from `"+"` to `"_ + _"` tries to be as minimalist as possible, and that plus the assumption that the default interpretation is picked is enough to explain what is happening.

#### Gaëtan Gilbert (Feb 15 2022 at 14:25):

the difference is the `strict` argument in https://github.com/coq/coq/blob/87f54b09c80566736b30471590cd20f702ed0558/interp/notation.ml#L2406

#### Emilio Jesús Gallego Arias (Feb 15 2022 at 14:43):

@Ana de Almeida Borges my reading of the code is that it searches all the keys that contain `+`

#### Emilio Jesús Gallego Arias (Feb 15 2022 at 14:43):

purely a string-based search

#### Ana de Almeida Borges (Feb 15 2022 at 17:54):

I will need to leave shortly. Will (any of) you be available tomorrow?

#### Emilio Jesús Gallego Arias (Feb 15 2022 at 17:57):

Yes @Ana de Almeida Borges

#### Ana de Almeida Borges (Feb 15 2022 at 17:58):

Cool! Same time as today (10:00 CET)?

#### Ali Caglayan (Feb 16 2022 at 09:36):

We are in Breakout room 2

#### Emilio Jesús Gallego Arias (Feb 16 2022 at 10:20):

`Notgram_ops.subentries_of_notation`

#### Emilio Jesús Gallego Arias (Feb 16 2022 at 10:20):

should be what we need for the 3rd parameter

#### Emilio Jesús Gallego Arias (Feb 16 2022 at 12:09):

@Hugo Herbelin we need your help

#### Ana de Almeida Borges (Feb 16 2022 at 17:21):

Today we updated our command so that it outputs the level and associativity information. :tada:

#### Ana de Almeida Borges (Feb 16 2022 at 17:22):

The information still needs to be made prettier, and the code as well, and we are thinking of adding extra information such as scopes.

#### Ana de Almeida Borges (Feb 16 2022 at 17:24):

Tomorrow morning I won't be able to make it at 10:00 CET either. I should be back before the afternoon sessions, but I can't predict when, sorry. In the meantime, anyone feel free to give your suggestions for what you would like this command to print and what could be improved.

#### Ana de Almeida Borges (Feb 16 2022 at 19:13):

By the way, is there any particular reason this should be called `Print Notation` and not, say, `About Notation` or `Check Notation`?

#### Ali Caglayan (Feb 16 2022 at 19:16):

It might be the case that `About Notation` is a more suitable command. `Print` typically just shows the underlying term of something, and `Check` prints a term typically with evars and typeclasses involved.

#### Ali Caglayan (Feb 16 2022 at 19:17):

Whatever it is, we should add a good documentation entry in the refman.

#### Gaëtan Gilbert (Feb 16 2022 at 19:19):

there are already a bunch of Print variants, no About or Check variants

#### Ali Caglayan (Feb 16 2022 at 19:24):

That's fair enough, I think sticking to print is better.

#### Ana de Almeida Borges (Feb 17 2022 at 10:19):

@Ali Caglayan @Emilio Jesús Gallego Arias I'm available now. Ping me if you want to / can go to a breakout room.

#### Ana de Almeida Borges (Feb 17 2022 at 10:51):

Here are some things a user might be interested in (using `"_ + _ "` as an example):

1. What does this notation mean? -- Answered by `Locate "+"` and also `Print "+"` (but with less information in a sense)
2. How is this notation parsed, or how does it work as a notation, not as whatever it is a notation for -- Answered by our current version of `Print Notation "_ + _"`
3. What is the notation for `Nat.add`? -- Not sure there is a better way than `Check (Nat.add 0 0)` and observing the output

#### Ana de Almeida Borges (Feb 17 2022 at 10:53):

I think it's reasonable to separate Concerns 1 and 2 into different commands. However, I (as a user) would prefer to type `Print Notation "+"` rather than `Print Notation "_ + _"`, and although I understand why the latter is better defined, I also think it's confusing from outside why the abbreviated version works with one command and not the other.

#### Ana de Almeida Borges (Feb 17 2022 at 10:56):

Allowing for under-specified notations would mean either giving information about all of them (like `Locate`), or picking the default one (like `Print`). Here is a quote from the PR:

Ali: There is the question of "Do we want to have multiple results?". I think it might be more prudent to have a Print Notation and Location Notation command. That way the latter can query like a locate command, but still return extra notation info.

#### Ana de Almeida Borges (Feb 17 2022 at 10:59):

@Ali Caglayan, were you thinking that this hypothetical `Locate Notation` would behave like our current `Print Notation` except it would give information about all the possible relevant notations? Or that it would give minimal information that would then be informative enough to pass to `Print Notation`?

#### Ana de Almeida Borges (Feb 17 2022 at 11:01):

I think Emilio was thinking the latter:

You could have a location command that returns the key, and a command that returns detailed info about the key

But he also said:

at some point vernac as query language doesn't cut it.

which I take to mean he thinks this is sub-optimal. And indeed I also think it would be annoying to try `Print Notation "+"`, get an error, sigh, do `Locate Notation "+"`, observe its key is `"_ + _"`, and finally do `Print Notation "_ + _"`.

#### Paolo Giarrusso (Feb 17 2022 at 11:02):

in fact, even today's `Locate` isn't complete enough:

``````Locate "map". (* Unknown notation *)
Locate "map]".
(*
Notation "'[∧' 'map]' x ∈ m , P" := (big_opM bi_and (fun _ x => P) m)
: bi_scope
... many other notations using `'map]'` as keyword
*)
``````

#### Paolo Giarrusso (Feb 17 2022 at 11:02):

I guess this needs a separate bug?

#### Pierre Roux (Feb 17 2022 at 12:36):

That may be a stupid question (I didn't participate to the discussions here): would it be possible for `Print Notation` to output separately a `Reserved Notation` with all the associativity and format information (not scope specific) and the `Notation`, with meaning (scope specific)?

#### Ali Caglayan (Feb 17 2022 at 12:39):

@Pierre Roux We are working in breakout room 3, join and we can discuss!

#### Emilio Jesús Gallego Arias (Feb 17 2022 at 12:51):

I think for now, I would just do as locate, try to get the key, if not, do some search using the key list, with substring or other mathcing

#### Emilio Jesús Gallego Arias (Feb 17 2022 at 12:51):

So actually we could have something like:

#### Emilio Jesús Gallego Arias (Feb 17 2022 at 12:52):

• the user types `Info Notation "+"`: the code tries to match for the key, if it fails, it returns a list of possible keys and prints something such as "Your query matches several notations, with keys .... . If you want more detailed information you can use this command with the particular key"

Last updated: Jun 11 2023 at 00:30 UTC