I am trying to understand when Coq prints a trailing space and when it does not...

There is a trailing space here but none here even though both of these notations are declared basically the same way. Can anyone explain that? :)

I guess @Hugo Herbelin is the right person for this question

(it's not terribly important, I would just like to understand)

interestingly, this MR https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/727 fixes the trailing space (as an unexpected side-effect of another change)

I'm not fully sure of the reason for the trailing spaces. I don't exclude that it is the OCaml formatter which sometimes print some before cutting. If you had a self-content reproducible example, that would be either to investigate!

@Hugo Herbelin here you go

```
From Coq Require Export Utf8.
(** * Turnstiles *)
Reserved Notation "P ⊢ Q" (at level 99, Q at level 200, right associativity).
Reserved Notation "P '⊢@{' PROP } Q" (at level 99, Q at level 200, right associativity).
Reserved Notation "(⊢)".
Reserved Notation "'(⊢@{' PROP } )".
Reserved Notation "( P ⊣⊢.)".
Reserved Notation "(.⊣⊢ Q )".
Reserved Notation "P ∗ Q" (at level 80, right associativity, format "P ∗ '/' Q").
Reserved Notation "'<pers>' P" (at level 20, right associativity).
Reserved Notation "▷ P" (at level 20, right associativity).
Reserved Notation "|={ E }=> Q"
(at level 99, E at level 50, Q at level 200,
format "'[ ' |={ E }=> '/' Q ']'").
Reserved Notation "P ={ E }=∗ Q"
(at level 99, E at level 50, Q at level 200,
format "'[' P ={ E }=∗ '/' Q ']'").
(** Define the scope *)
Declare Scope bi_scope.
Delimit Scope bi_scope with I.
Section test.
Context (PROP : Type).
Context (bi_entails : PROP → PROP → Prop).
Context (bi_sep : PROP → PROP → PROP).
Context (bi_later : PROP → PROP).
Context (bi_persistently : PROP → PROP).
Context (fupd : nat → nat → PROP → PROP).
Notation "P ⊢ Q" := (bi_entails P%I Q%I).
Infix "∗" := bi_sep : bi_scope.
Notation "'<pers>' P" := (bi_persistently P) : bi_scope.
Notation "▷ P" := (bi_later P) : bi_scope.
Notation "|={ E }=> Q" := (fupd E E Q) : bi_scope.
Notation "P ={ E }=∗ Q" := (P ⊢ |={E}=> Q).
Context (na_inv : nat → nat → PROP → PROP).
Context (na_own : nat → nat → PROP).
Lemma test_iInv_4_with_close t N E1 E2 P:
N ≤ E2 →
na_inv t N (<pers> P) ∗ na_own t E1 ∗ na_own t E2
⊢ |={0}=> na_own t E1 ∗ na_own t E2 ∗ ▷ P.
Proof.
Set Printing Width 80.
```

I checked and Coq does not send a space to OCaml's formatter. So, the hypothesis is that it is OCaml which adds space. If it is e.g. to be consistent with git rules standardizing spacing that you'd like this space not to occur, and if it is confirmed that it is added by OCaml, a PR to their file `format.ml`

could maybe be submitted!

git highlights the trailing space as red in the diff, but it doesnt really cause problems

so I don't think I'll sink more time into this. it just could have been that there is something to be learned here about the formatting machinery that I did not know yet. :)

Last updated: May 24 2024 at 22:02 UTC