Stream: Coq users

Topic: Trailing spaces in notation

view this post on Zulip Ralf Jung (Jul 29 2021 at 07:31):

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? :)

view this post on Zulip Ralf Jung (Jul 29 2021 at 07:34):

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

view this post on Zulip Ralf Jung (Jul 29 2021 at 08:58):

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

view this post on Zulip Ralf Jung (Jul 29 2021 at 09:25):

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)

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 11:01):

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!

view this post on Zulip Ralf Jung (Jul 29 2021 at 12:22):

@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.

view this post on Zulip Hugo Herbelin (Jul 30 2021 at 08:24):

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!

view this post on Zulip Ralf Jung (Jul 30 2021 at 12:00):

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

view this post on Zulip Ralf Jung (Jul 30 2021 at 12:00):

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: Sep 15 2024 at 13:02 UTC