bad pretty printing result

[tomtomjhj]

big stuff ≡{n}≡ big stuff looks bad (when proving Contractive stuff)

big stuff ≡{n}≡ big
                  stuff

while big stuff = big stuff is fine.

big stuff =
big stuff

Both look good on coqide.

This happens because the former doesn't have explicit break after ≡{n}≡. Instead, it gets { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", " " } }.

{ "Ppcmd_glue", {
    { "Ppcmd_box", { "Pp_hovbox", 2 }, { "Ppcmd_glue", {
        ...
    } } },
    { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", " " } }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", "≡{" } }, { "Ppcmd_tag", "constr.variable", { "Ppcmd_string", "n" } }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", "}≡" } }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", " " } },
    { "Ppcmd_box", { "Pp_hovbox", 2 }, { "Ppcmd_glue", {
        ...
    } } }
} }

On the other hand, = gets a break after =.

{ "Ppcmd_box", { "Pp_hovbox", 0 }, { "Ppcmd_glue", {
    { "Ppcmd_box", { "Pp_hovbox", 2 }, { "Ppcmd_glue", {
        ...
    } } },
    { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", " =" } }, { "Ppcmd_print_break", 1, 0 },
    { "Ppcmd_box", { "Pp_hovbox", 2 }, { "Ppcmd_glue", {
        ...
    } } }
} } }

Maybe n prevents inserting break? Or is there a special treatment for builtin notations?

Notation "x = y" := (eq x y) : type_scope.
Notation "x ≡{ n }≡ y" := (dist n x y)
  (at level 70, n at next level, format "x  ≡{ n }≡  y").

Make an issue on iris to add '/'?

Why does it look correct in coqdie???

other bad formatting examples.

• VsCoq search Persistent

[tomtomjhj]

All the results are the same in coqidetop and vscoqtop, in contrast to the observation on the top post.

Definition F (q w e r t y u i o p : nat) : nat := 0.

(* Notation "x = y" := (eq x y) : type_scope. *)
Goal F 111 111 111 111 111 111 111 111 111 111 = F 111 111 111 111 111 111 111 111 111 111.
(*
F 111 111 111 111 111 111 111 111 111 111 =
F 111 111 111 111 111 111 111 111 111 111
*)
Abort.

Definition equiv (x y : nat) := True.

Notation "x ≡ y" := (equiv x y) (at level 70).
Goal F 111 111 111 111 111 111 111 111 111 111 ≡ F 111 111 111 111 111 111 111 111 111 111.
(*
F 111 111 111 111 111 111 111 111 111 111
≡ F 111 111 111 111 111 111 111 111 111 111

> For printing a notation, a formatting box is opened in such a way that if the
> notation and its arguments cannot fit on a single line, a line break is
> inserted before the symbols of the notation and the arguments on the next lines
> are aligned with the argument on the first line.

Question: Why does "x = y" notation above has break after "="?
*)
Abort.

(*
> 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.
*)

Notation "x  ≡  y" := (equiv x y) (at level 70).
Goal F 111 111 111 111 111 111 111 111 111 111 ≡ F 111 111 111 111 111 111 111 111 111 111.
(*
F 111 111 111 111 111 111 111 111 111 111 ≡
F 111 111 111 111 111 111 111 111 111 111

Question: Why does this change the location of break point?
*)
Abort.

Notation "x ≡ y" := (equiv x y) (at level 70, format "x  ≡  y").
Goal F 111 111 111 111 111 111 111 111 111 111 ≡ F 111 111 111 111 111 111 111 111 111 111.
(*
F 111 111 111 111 111 111 111 111 111 111 ≡ F 111 111 111 111 111 111 111 111
                                              111 111

Question: Why no break point???
*)
Abort.

Notation "x ≡ y" := (equiv x y) (at level 70, format "'[' x  ≡ '/' y ']'").
Goal F 111 111 111 111 111 111 111 111 111 111 ≡ F 111 111 111 111 111 111 111 111 111 111.
(*
F 111 111 111 111 111 111 111 111 111 111 ≡
F 111 111 111 111 111 111 111 111 111 111
*)
Abort.

Goal F 1 1 1 1 1 1 1 1 1 1 ≡ F 1 1 1 1 1 1 1 1 1 1.
(*
F 1 1 1 1 1 1 1 1 1 1 ≡F 1 1 1 1 1 1 1 1 1 1

NOTE: '/' itself doesn't occupy space.
*)
Abort.

[tomtomjhj]

Query results don't have proper breaks. :VsCoq about wp_fupd.

{ "Ppcmd_box", { "Pp_vbox", 0 }, { "Ppcmd_glue", { { "Ppcmd_box", { "Pp_hovbox", 0 }, { "Ppcmd_glue", { { "Ppcmd_string", "wp_fupd" }, { "Ppcmd_string", " :" }, { "Ppcmd_print_break", 1, 0 }, { "Ppcmd_box", { "Pp_hovbox", 2 }, { "Ppcmd_glue", { { "Ppcmd_box", { "Pp_hovbox", 2 }, { "Ppcmd_glue", { { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", "∀" } }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", " " } }, { "Ppcmd_box", { "Pp_hovbox", 1 }, { "Ppcmd_glue", { { "Ppcmd_string", "{" }, { "Ppcmd_string", "hlc" }, { "Ppcmd_string", " : " }, { "Ppcmd_tag", "constr.variable", { "Ppcmd_string", "has_lc" } }, { "Ppcmd_string", "}" } } } }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", " " } }, { "Ppcmd_box", { "Pp_hovbox", 1 }, { "Ppcmd_glue", { { "Ppcmd_string", "{" }, { "Ppcmd_string", "Λ" }, { "Ppcmd_string", " : " }, { "Ppcmd_tag", "constr.variable", { "Ppcmd_string", "language" } }, { "Ppcmd_string", "}" } } } }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", " " } }, { "Ppcmd_box", { "Pp_hovbox", 1 }, { "Ppcmd_glue", { { "Ppcmd_string", "{" }, { "Ppcmd_string", "Σ" }, { "Ppcmd_string", " : " }, { "Ppcmd_tag", "constr.variable", { "Ppcmd_string", "gFunctors" } }, { "Ppcmd_string", "}" } } } }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", " " } }, { "Ppcmd_box", { "Pp_hovbox", 1 }, { "Ppcmd_glue", { { "Ppcmd_string", "{" }, { "Ppcmd_string", "irisGS_gen0" }, { "Ppcmd_string", " : " }, { "Ppcmd_box", { "Pp_hovbox", 2 }, { "Ppcmd_glue", { { "Ppcmd_tag", "constr.variable", { "Ppcmd_string", "irisGS_gen" } }, { "Ppcmd_print_break", 1, 0 }, { "Ppcmd_tag", "constr.variable", { "Ppcmd_string", "hlc" } }, { "Ppcmd_print_break", 1, 0 }, { "Ppcmd_tag", "constr.variable", { "Ppcmd_string", "Λ" } }, { "Ppcmd_print_break", 1, 0 }, { "Ppcmd_tag", "constr.variable", { "Ppcmd_string", "Σ" } } } } }, { "Ppcmd_string", "}" } } } }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", " " } }, { "Ppcmd_box", { "Pp_hovbox", 1 }, { "Ppcmd_glue", { { "Ppcmd_string", "(" }, { "Ppcmd_string", "s" }, { "Ppcmd_string", " : " }, { "Ppcmd_tag", "constr.variable", { "Ppcmd_string", "stuckness" } }, { "Ppcmd_string", ")" } } } }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", " " } }, { "Ppcmd_box", { "Pp_hovbox", 1 }, { "Ppcmd_glue", { { "Ppcmd_string", "(" }, { "Ppcmd_string", "E" }, { "Ppcmd_string", " : " }, { "Ppcmd_tag", "constr.variable", { "Ppcmd_string", "coPset" } }, { "Ppcmd_string", ")" } } } }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", " " } }, { "Ppcmd_box", { "Pp_hovbox", 1 }, { "Ppcmd_glue", { { "Ppcmd_string", "(" }, { "Ppcmd_string", "e" }, { "Ppcmd_string", " : " }, { "Ppcmd_box", { "Pp_hovbox", 0 }, { "Ppcmd_glue", { { "Ppcmd_tag", "constr.variable", { "Ppcmd_string", "Λ" } }, { "Ppcmd_print_break", 0, 0 }, { "Ppcmd_string", ".(" }, { "Ppcmd_box", { "Pp_hovbox", 2 }, { "Ppcmd_glue", { { "Ppcmd_tag", "constr.path", { "Ppcmd_string", "language" } }, { "Ppcmd_string", "." }, { "Ppcmd_tag", "constr.reference", { "Ppcmd_string", "expr" } } } } }, { "Ppcmd_string", ")" } } } }, { "Ppcmd_string", ")" } } } }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", " " } }, { "Ppcmd_box", { "Pp_hovbox", 1 }, { "Ppcmd_glue", { { "Ppcmd_string", "(" }, { "Ppcmd_string", "Φ" }, { "Ppcmd_string", " : " }, { "Ppcmd_box", { "Pp_hovbox", 0 }, { "Ppcmd_glue", { { "Ppcmd_box", { "Pp_hovbox", 0 }, { "Ppcmd_glue", { { "Ppcmd_tag", "constr.variable", { "Ppcmd_string", "Λ" } }, { "Ppcmd_print_break", 0, 0 }, { "Ppcmd_string", ".(" }, { "Ppcmd_box", { "Pp_hovbox", 2 }, { "Ppcmd_glue", { { "Ppcmd_tag", "constr.path", { "Ppcmd_string", "language" } }, { "Ppcmd_string", "." }, { "Ppcmd_tag", "constr.reference", { "Ppcmd_string", "val" } } } } }, { "Ppcmd_string", ")" } } } }, { "Ppcmd_print_break", 1, 0 }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", "→ " } }, { "Ppcmd_box", { "Pp_hovbox", 2 }, { "Ppcmd_glue", { { "Ppcmd_tag", "constr.variable", { "Ppcmd_string", "iProp" } }, { "Ppcmd_print_break", 1, 0 }, { "Ppcmd_tag", "constr.variable", { "Ppcmd_string", "Σ" } } } } } } } }, { "Ppcmd_string", ")" } } } } } } }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", "," } }, { "Ppcmd_print_break", 1, 0 }, { "Ppcmd_box", { "Pp_hovbox", 0 }, { "Ppcmd_glue", { { "Ppcmd_box", { "Pp_hvbox", 0 }, { "Ppcmd_glue", { { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", "WP" } }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", " " } }, { "Ppcmd_tag", "constr.variable", { "Ppcmd_string", "e" } }, { "Ppcmd_print_break", 1, 0 }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", "@" } }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", " " } }, { "Ppcmd_box", { "Pp_hovbox", 0 }, { "Ppcmd_glue", { { "Ppcmd_tag", "constr.variable", { "Ppcmd_string", "s" } }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", ";" } }, { "Ppcmd_print_break", 1, 0 }, { "Ppcmd_tag", "constr.variable", { "Ppcmd_string", "E" } }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", " " } } } } }, { "Ppcmd_print_break", 0, 0 }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", "{{" } }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", " " } }, { "Ppcmd_box", { "Pp_hovbox", 0 }, { "Ppcmd_glue", { { "Ppcmd_tag", "constr.variable", { "Ppcmd_string", "v" } }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", "," } }, { "Ppcmd_print_break", 1, 0 }, { "Ppcmd_box", { "Pp_hovbox", 2 }, { "Ppcmd_glue", { { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", "|={" } }, { "Ppcmd_tag", "constr.variable", { "Ppcmd_string", "E" } }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", "}=>" } }, { "Ppcmd_print_break", 1, 0 }, { "Ppcmd_box", { "Pp_hovbox", 2 }, { "Ppcmd_glue", { { "Ppcmd_tag", "constr.variable", { "Ppcmd_string", "Φ" } }, { "Ppcmd_print_break", 1, 0 }, { "Ppcmd_tag", "constr.variable", { "Ppcmd_string", "v" } } } } } } } }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", " " } } } } }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_glue", { { "Ppcmd_string", "}" }, { "Ppcmd_string", "}" } } } } } } }, { "Ppcmd_print_break", 1, 0 }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", "⊢ " } }, { "Ppcmd_box", { "Pp_hvbox", 0 }, { "Ppcmd_glue", { { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", "WP" } }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", " " } }, { "Ppcmd_tag", "constr.variable", { "Ppcmd_string", "e" } }, { "Ppcmd_print_break", 1, 0 }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", "@" } }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", " " } }, { "Ppcmd_box", { "Pp_hovbox", 0 }, { "Ppcmd_glue", { { "Ppcmd_tag", "constr.variable", { "Ppcmd_string", "s" } }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", ";" } }, { "Ppcmd_print_break", 1, 0 }, { "Ppcmd_tag", "constr.variable", { "Ppcmd_string", "E" } }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", " " } } } } }, { "Ppcmd_print_break", 0, 0 }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", "{{" } }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", " " } }, { "Ppcmd_box", { "Pp_hovbox", 0 }, { "Ppcmd_glue", { { "Ppcmd_tag", "constr.variable", { "Ppcmd_string", "v" } }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", "," } }, { "Ppcmd_print_break", 1, 0 }, { "Ppcmd_box", { "Pp_hovbox", 2 }, { "Ppcmd_glue", { { "Ppcmd_tag", "constr.variable", { "Ppcmd_string", "Φ" } }, { "Ppcmd_print_break", 1, 0 }, { "Ppcmd_tag", "constr.variable", { "Ppcmd_string", "v" } } } } }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_string", " " } } } } }, { "Ppcmd_tag", "constr.notation", { "Ppcmd_glue", { { "Ppcmd_string", "}" }, { "Ppcmd_string", "}" } } } } } } } } } } } } } } } }, { "Ppcmd_print_break", 0, 0 }, { "Ppcmd_print_break", 0, 0 }, { "Ppcmd_string", "wp_fupd" }, { "Ppcmd_string", " is " }, { "Ppcmd_string", "not universe polymorphic" }, { "Ppcmd_print_break", 0, 0 }, { "Ppcmd_box", { "Pp_hovbox", 2 }, { "Ppcmd_glue", { { "Ppcmd_string", "Arguments" }, { "Ppcmd_print_break", 1, 0 }, { "Ppcmd_tag", "constr.reference", { "Ppcmd_string", "wp_fupd" } }, { "Ppcmd_print_break", 1, 0 }, { "Ppcmd_box", { "Pp_hovbox", 1 }, { "Ppcmd_glue", { { "Ppcmd_string", "{" }, { "Ppcmd_string", "" }, { "Ppcmd_string", "hlc" }, { "Ppcmd_print_break", 1, 0 }, { "Ppcmd_string", "" }, { "Ppcmd_string", "Λ" }, { "Ppcmd_print_break", 1, 0 }, { "Ppcmd_string", "" }, { "Ppcmd_string", "Σ" }, { "Ppcmd_print_break", 1, 0 }, { "Ppcmd_string", "" }, { "Ppcmd_string", "irisGS_gen0" }, { "Ppcmd_string", "}" } } } }, { "Ppcmd_print_break", 1, 0 }, { "Ppcmd_box", { "Pp_hovbox", 1 }, { "Ppcmd_glue", { { "Ppcmd_string", "" }, { "Ppcmd_string", "s" } } } }, { "Ppcmd_print_break", 1, 0 }, { "Ppcmd_box", { "Pp_hovbox", 1 }, { "Ppcmd_glue", { { "Ppcmd_string", "" }, { "Ppcmd_string", "E" } } } }, { "Ppcmd_print_break", 1, 0 }, { "Ppcmd_box", { "Pp_hovbox", 1 }, { "Ppcmd_glue", { { "Ppcmd_string", "" }, { "Ppcmd_string", "e" }, { "Ppcmd_string", "%" }, { "Ppcmd_string", "expr_scope" } } } }, { "Ppcmd_print_break", 1, 0 }, { "Ppcmd_box", { "Pp_hovbox", 1 }, { "Ppcmd_glue", { { "Ppcmd_string", "" }, { "Ppcmd_string", "Φ" }, { "Ppcmd_string", "%" }, { "Ppcmd_string", "function_scope" } } } }, { "Ppcmd_string", "" } } } }, { "Ppcmd_print_break", 0, 0 }, { "Ppcmd_string", "wp_fupd" }, { "Ppcmd_string", " is " }, { "Ppcmd_string", "opaque" }, { "Ppcmd_print_break", 0, 0 }, { "Ppcmd_box", { "Pp_hovbox", 0 }, { "Ppcmd_glue", { { "Ppcmd_string", "Expands to: " }, { "Ppcmd_string", "Constant" }, { "Ppcmd_print_break", 1, 0 }, { "Ppcmd_string", "iris.program_logic.weakestpre.wp_fupd" } } } } } } }

wp_fupd :
∀ {hlc : has_lc} {Λ : language} {Σ : gFunctors} {irisGS_gen0 : irisGS_gen hlc Λ Σ} (s : stuckness) (E : coPset) (e : Λ
                                                                                                                     .(language.expr)) (Φ : Λ
                                                                                                                                            .(language.val)
                                                                                                                                            → iProp
                                                                                                                                                Σ),
  WP e @ s; E {{ v, |={E}=> Φ v }} ⊢ WP e @ s; E {{ v, Φ v }}

On the other hand, hover result is pre-formatted.

```coq
∀ {hlc : has_lc} {Λ : language} {Σ : gFunctors} {irisGS_gen0 : 
                                                 irisGS_gen hlc Λ Σ} 
  (s : stuckness) (E : coPset) (e : Λ.(language.expr)) 
  (Φ : Λ.(language.val) → iProp Σ),
  WP e @ s; E {{ v, |={E}=> Φ v }} ⊢ WP e @ s; E {{ v, Φ v }}

───────────────────────────────────────────────────────────────────── Args: {hlc Λ Σ irisGS_gen0} s E e%expr_scope Φ%function_scope ───────────────────────────────────────────────────────────────────── Constant iris.program_logic.weakestpre.wp_fupd

[tomtomjhj]

Ppcmd_string string may contain newline. :VsCoq about elim_modal_fupd_wp_wrong_mask.

Fixed