Stream: Coq users

Topic: Notation printing: space control without `format`


view this post on Zulip Ralf Jung (Nov 29 2021 at 19:21):

I recently learned that one can, to some extend, control the spacing in printing of Notation even without giving a format. That would be great, since format is rather redundant -- almost every change to the notation required adjusting both the notation and the format (the format contains strictly more information and one could easily compute the notation from it... at least in the cases I have seen, which includes some tricky iris notation).
So I tried using this but I don't understand how it works. I looked at the docs and they dont explain it either. The example there in fact is very strange:

Notation "{{  x : A | P  }}" := (sig (fun x : A => P)) (at level 0, x at level 99).

Check (sig (fun x : nat => x=x)).
(* prints *)
    {{ x : nat | x = x }}
         : Set

So note that the printing adds a space everywhere but Notation has 2 spaces only in some places! What I expected this definition to print is {{ x:nat|x=x }}, since that matches the notation when interrpreted as a format string.

I was hoping I could simplify defining notation like

Notation "●U_ q a" := (ufrac_auth_auth q a) (at level 10, q at level 9, format "●U_ q  a").

to

Notation "●U_ q  a" := (ufrac_auth_auth q a) (at level 10, q at level 9).

but now Coq still adds a space after the _.

How does Coq decide whether to put a space between two symbols or not? My assumption was that once I use a double-space anywhere in the notation, this is fully under my control, but in fact there seem to be some heuristics that add extra spaces which make "space control without format" basically useless in practice, hence causing redundancy for each notation definition.

view this post on Zulip Gaëtan Gilbert (Nov 29 2021 at 19:25):

My assumption was that once I use a double-space anywhere in the notation, this is fully under my control

I assumed that it would use whatever the heuristic is except for the double space occurences

view this post on Zulip Gaëtan Gilbert (Nov 29 2021 at 19:25):

is that not how it works?

view this post on Zulip Paolo Giarrusso (Nov 29 2021 at 19:54):

Also my recollection — you get the default pretty-printing except that 2 spaces force an extra one, which is a more “continuous” semantics than what you describe.

view this post on Zulip Paolo Giarrusso (Nov 29 2021 at 19:55):

You’re basically asking for action at a distance: adding two spaces in one spot would affect printing in completely different spots.

view this post on Zulip Gaëtan Gilbert (Nov 29 2021 at 19:56):

https://coq.github.io/doc/master/refman/user-extensions/syntax-extensions.html#use-of-notations-for-printing

A first, simple control that a user can have on the printing of a notation is the insertion of spaces at some places of the notation. This is performed by adding extra spaces between the symbols and parameters: each extra space (other than the single space needed to separate the components) is interpreted as a space to be inserted by the printer. Here is an example showing how to add spaces next to the curly braces.

view this post on Zulip Paolo Giarrusso (Nov 29 2021 at 19:56):

your example makes sense, but a better fix for that seems to add a “no space here” escape (if we can somehow find one).

view this post on Zulip Ralf Jung (Nov 29 2021 at 19:56):

well I am mostly asking for a non-redundant way to actually control spaces :)

view this post on Zulip Ralf Jung (Nov 29 2021 at 19:56):

where 'control' also includes not having a space somewhere that the default heuristic puts one

view this post on Zulip Ralf Jung (Nov 29 2021 at 19:57):

FWIW I didnt even know there is a heuristic, I thought it was just one space between all parts of the notation

view this post on Zulip Gaëtan Gilbert (Nov 29 2021 at 19:57):

also why is that doc showing errors o_o

view this post on Zulip Ralf Jung (Nov 29 2021 at 19:58):

the docs do not say that there is any 'heuristic' of sorts that would do anything clever when nothing is specified manually

view this post on Zulip Ralf Jung (Nov 29 2021 at 19:59):

Gaëtan Gilbert said:

also why is that doc showing errors o_o

what do you mean?

view this post on Zulip Gaëtan Gilbert (Nov 29 2021 at 20:00):

https://github.com/coq/coq/issues/15264

view this post on Zulip Ralf Jung (Nov 29 2021 at 20:00):

Paolo Giarrusso said:

your example makes sense, but a better fix for that seems to add a “no space here” escape (if we can somehow find one).

an alternative might be something like format integrated (keyword open for bikeshedding) which changes the main notation string to be interpreted like the format string would, i.e. a single space means "no space" -- and possible one could even use boxes there

view this post on Zulip Ralf Jung (Nov 29 2021 at 20:01):

it would be a bit annoying to add format integrated to every single notation, but it'd still be better than the redundancy that we currently have instead

view this post on Zulip Paolo Giarrusso (Nov 29 2021 at 20:01):

I guess one needs to design a tasteful way to distinguish box characters meant for boxes and box characters meant as literals.

view this post on Zulip Ralf Jung (Nov 29 2021 at 20:02):

oh right the ' are not sufficient for that in the main format string

view this post on Zulip Ralf Jung (Nov 29 2021 at 20:03):

but independent of all that the docs the extra spaces in the main notation string is confusing:

Here is an example showing how to add spaces next to the curly braces.

that example has spaces everywhere, even when there are no double-spaces in the notation! without knowing the 'default heuristic' (the existence of which is not even mentioned) it is entirely unclear what is even happening here

view this post on Zulip Paolo Giarrusso (Nov 29 2021 at 20:04):

so what changes if you drop the extra spaces?

view this post on Zulip Ralf Jung (Nov 29 2021 at 20:05):

it becomes {{x : nat | x = x}}

view this post on Zulip Ralf Jung (Nov 29 2021 at 20:05):

no idea why that is a sensible heuristic...

view this post on Zulip Paolo Giarrusso (Nov 29 2021 at 20:06):

looks reasonable to me, but no idea either.

view this post on Zulip Paolo Giarrusso (Nov 29 2021 at 20:07):

we don’t have docs for the inference of levels, and those one seem even more essential, since you need those when making notations left-factorable…

view this post on Zulip Paolo Giarrusso (Nov 29 2021 at 20:07):

I recall @Jim Fehrle once implied that one can’t really learn to use Coq by black-box reverse engineering, and I think I was like “what’s the alternative?”

view this post on Zulip Ralf Jung (Nov 29 2021 at 20:07):

it doesnt look reasonable to be TBH -- not sure why one would skip those spaces but not e.g. also the ones around |

view this post on Zulip Ralf Jung (Nov 29 2021 at 20:08):

Paolo Giarrusso said:

we don’t have docs for the inference of levels, and those one seem even more essential, since you need those when making notations left-factorable…

yeah well that stuff is black magic that I dont even begin to understand. format strings on the other hand actually make sense to me. ;)

view this post on Zulip Paolo Giarrusso (Nov 29 2021 at 20:08):

I’m not really sure, but it seems the spacing I’d want to get in LaTeX :-)

view this post on Zulip Paolo Giarrusso (Nov 29 2021 at 20:09):

e.g. for set builder notation, {x | x <> 0} is the canonical spacing.

view this post on Zulip Ralf Jung (Nov 29 2021 at 20:09):

says who? looks wrong to me^^

view this post on Zulip Ralf Jung (Nov 29 2021 at 20:11):

but anyway that is clearly a matter of taste

view this post on Zulip Ralf Jung (Nov 29 2021 at 20:11):

my biggest surprise was that there is a heuristic at all here, rather than just saying 'one space between all parts of the notation'

view this post on Zulip Paolo Giarrusso (Nov 29 2021 at 20:11):

maths has typographic rules, and by default, all binary operators _and_ relation operators need spaces around — that’s the policy in both TeX and normal PLs

view this post on Zulip Paolo Giarrusso (Nov 29 2021 at 20:13):

I agree that both undocumented heuristics here should ideally at least be documented, we just have more basic problems to fix :-)

view this post on Zulip Paolo Giarrusso (Nov 29 2021 at 20:14):

(and Coq _is_ making lots of progress!)

view this post on Zulip Paolo Giarrusso (Nov 29 2021 at 20:17):

for instance, an automated pretty-printer suitable for source-code formatting would be very nice.

view this post on Zulip Ralf Jung (Nov 29 2021 at 20:19):

Paolo Giarrusso said:

maths has typographic rules, and by default, all binary operators _and_ relation operators need spaces around — that’s the policy in both TeX and normal PLs

TeX has mutliple kinds of spacing of different width, I dont think you can easily translate that to ASCII formatting


Last updated: Feb 04 2023 at 21:02 UTC