Ana de Almeida Borges (Feb 15 2022 at 09:42): 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 11:08):cf. https://github.com/coq/coq/wiki/CoqWG-Activity
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 "+".
(*
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.
Gaëtan Gilbert (Feb 15 2022 at 14:22):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
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):
Locate "+" and also Print "+" (but with less information in a sense)Print Notation "_ + _"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
*)
I guess this needs a separate bug?
Paolo Giarrusso (Feb 17 2022 at 11:59):filed as https://github.com/coq/coq/issues/15705
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):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