Ralf Jung (Nov 29 2021 at 19:21): 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.
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
Gaëtan Gilbert (Nov 29 2021 at 19:25):is that not how it works?
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.
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.
Gaëtan Gilbert (Nov 29 2021 at 19:56):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.
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).
Ralf Jung (Nov 29 2021 at 19:56):well I am mostly asking for a non-redundant way to actually control spaces :)
Ralf Jung (Nov 29 2021 at 19:56):where 'control' also includes not having a space somewhere that the default heuristic puts one
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
Gaëtan Gilbert (Nov 29 2021 at 19:57):also why is that doc showing errors o_o
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
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?
Gaëtan Gilbert (Nov 29 2021 at 20:00):https://github.com/coq/coq/issues/15264
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
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
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.
Ralf Jung (Nov 29 2021 at 20:02):oh right the ' are not sufficient for that in the main format string
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
Paolo Giarrusso (Nov 29 2021 at 20:04):so what changes if you drop the extra spaces?
Ralf Jung (Nov 29 2021 at 20:05):it becomes {{x : nat | x = x}}
Ralf Jung (Nov 29 2021 at 20:05):no idea why that is a sensible heuristic...
Paolo Giarrusso (Nov 29 2021 at 20:06):looks reasonable to me, but no idea either.
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…
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?”
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 |
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. ;)
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 :-)
Paolo Giarrusso (Nov 29 2021 at 20:09):e.g. for set builder notation, {x | x <> 0} is the canonical spacing.
Ralf Jung (Nov 29 2021 at 20:09):says who? looks wrong to me^^
Ralf Jung (Nov 29 2021 at 20:11):but anyway that is clearly a matter of taste
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'
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
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 :-)
Paolo Giarrusso (Nov 29 2021 at 20:14):(and Coq _is_ making lots of progress!)
Paolo Giarrusso (Nov 29 2021 at 20:17):for instance, an automated pretty-printer suitable for source-code formatting would be very nice.
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: Sep 26 2023 at 12:02 UTC