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?

I would be happy to help

I can also too Ana

maybe that would be a good topic

I need 10 minutes and I join you folks

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

cf. https://github.com/coq/coq/wiki/CoqWG-Activity

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

`"+"`

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 "+".
(*
Nat.add =
fix add (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| S p => S (add p m)
end
: nat -> nat -> nat
Arguments Nat.add (n m)%nat_scope
*)
```

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.

yes

https://github.com/coq/coq/blob/87f54b09c80566736b30471590cd20f702ed0558/vernac/prettyp.ml#L926 calls https://github.com/coq/coq/blob/87f54b09c80566736b30471590cd20f702ed0558/interp/notation.ml#L2444 with the filtering done at https://github.com/coq/coq/blob/87f54b09c80566736b30471590cd20f702ed0558/interp/notation.ml#L2456-L2462

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.

the difference is the `strict`

argument in https://github.com/coq/coq/blob/87f54b09c80566736b30471590cd20f702ed0558/interp/notation.ml#L2406

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

purely a string-based search

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

Yes @Ana de Almeida Borges

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

We are in Breakout room 2

`Notgram_ops.subentries_of_notation`

should be what we need for the 3rd parameter

@Hugo Herbelin we need your help

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

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

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.

By the way, is there any particular reason this should be called `Print Notation`

and not, say, `About Notation`

or `Check Notation`

?

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.

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

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

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

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

Here are some things a user might be interested in (using `"_ + _ "`

as an example):

- What does this notation mean? -- Answered by
`Locate "+"`

and also`Print "+"`

(but with less information in a sense) - 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 "_ + _"`

- What is the notation for
`Nat.add`

? -- Not sure there is a better way than`Check (Nat.add 0 0)`

and observing the output

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.

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.

@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`

?

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 "_ + _"`

.

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
*)
```

I guess this needs a separate bug?

filed as https://github.com/coq/coq/issues/15705

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

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

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

So actually we could have something like:

- 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: Jan 29 2023 at 16:02 UTC