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.

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

is that not how it works?

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.

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

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.

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

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

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

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

also why is that doc showing errors o_o

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

Gaëtan Gilbert said:

also why is that doc showing errors o_o

what do you mean?

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

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

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

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

oh right the `'`

are not sufficient for that in the main format string

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

so what changes if you drop the extra spaces?

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

no idea why that is a sensible heuristic...

looks reasonable to me, but no idea either.

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…

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

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

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. ;)

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

e.g. for set builder notation, `{x | x <> 0}`

is the canonical spacing.

says who? looks wrong to me^^

but anyway that is clearly a matter of taste

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

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

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

(and Coq _is_ making lots of progress!)

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

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: Sep 26 2023 at 12:02 UTC