Stream: Coq Hackathon and Working Group, Winter 2022

Topic: Print Notation command


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

view this post on Zulip Ali Caglayan (Feb 15 2022 at 09:44):

I would be happy to help

view this post on Zulip Emilio Jesús Gallego Arias (Feb 15 2022 at 09:44):

I can also too Ana

view this post on Zulip Emilio Jesús Gallego Arias (Feb 15 2022 at 09:44):

maybe that would be a good topic

view this post on Zulip Emilio Jesús Gallego Arias (Feb 15 2022 at 09:45):

I need 10 minutes and I join you folks

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

view this post on Zulip Ana de Almeida Borges (Feb 15 2022 at 11:08):

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

view this post on Zulip Ana de Almeida Borges (Feb 15 2022 at 13:06):

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

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

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

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 15 2022 at 14:43):

purely a string-based search

view this post on Zulip Ana de Almeida Borges (Feb 15 2022 at 17:54):

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 15 2022 at 17:57):

Yes @Ana de Almeida Borges

view this post on Zulip Ana de Almeida Borges (Feb 15 2022 at 17:58):

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

view this post on Zulip Ali Caglayan (Feb 16 2022 at 09:36):

We are in Breakout room 2

view this post on Zulip Emilio Jesús Gallego Arias (Feb 16 2022 at 10:20):

Notgram_ops.subentries_of_notation

view this post on Zulip Emilio Jesús Gallego Arias (Feb 16 2022 at 10:20):

should be what we need for the 3rd parameter

view this post on Zulip Emilio Jesús Gallego Arias (Feb 16 2022 at 12:09):

@Hugo Herbelin we need your help

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

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

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

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

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

view this post on Zulip Ali Caglayan (Feb 16 2022 at 19:17):

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

view this post on Zulip Gaëtan Gilbert (Feb 16 2022 at 19:19):

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

view this post on Zulip Ali Caglayan (Feb 16 2022 at 19:24):

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

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

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

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

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

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

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

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

view this post on Zulip Paolo Giarrusso (Feb 17 2022 at 11:02):

I guess this needs a separate bug?

view this post on Zulip Paolo Giarrusso (Feb 17 2022 at 11:59):

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

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

view this post on Zulip Ali Caglayan (Feb 17 2022 at 12:39):

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 17 2022 at 12:51):

So actually we could have something like:

view this post on Zulip Emilio Jesús Gallego Arias (Feb 17 2022 at 12:52):


Last updated: Jan 29 2023 at 16:02 UTC