Stream: Coq users

Topic: Strange newline in printing


view this post on Zulip Ralf Jung (Jul 27 2021 at 14:50):

I am seeing a newline being added in printing where none should be:

  Σ : gFunctors
  heapGS0 : heapGS Σ
  l : loc
  ============================
  --------------------------------------
  |={}=>
  True

There's more than enough space to put |={⊤}=> True on one line, so why is it adding a newline?
The notation is declared like this

Reserved Notation "|={ E }=> Q"
  (at level 99, E at level 50, Q at level 200,
   format "|={ E }=>  '/' Q").

so it should only put a newline when there is not enough space.
I tried to reproduce this in a self-contained file but the same notations seem to behave differently there. Any idea what might be going on?
Cc @Hugo Herbelin

view this post on Zulip Guillaume Melquiond (Jul 27 2021 at 15:39):

How is the notation for -----* defined? If it is using a v or hv box, since your notation is not using any box, the excessive length of -----* will cause the break of your notation to act as a vertical break.

view this post on Zulip Ralf Jung (Jul 27 2021 at 16:11):

@Guillaume Melquiond no boxes there

Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" :=
  (envs_entails (Envs Γ Δ _) Q%I)
  (at level 1, Q at level 200, left associativity,
  format "Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ∗ '//' Q '//'", only printing) :
  stdpp_scope.
Notation "Δ '--------------------------------------' ∗ Q" :=
  (envs_entails (Envs Enil Δ _) Q%I)
  (at level 1, Q at level 200, left associativity,
  format "Δ '--------------------------------------' ∗ '//' Q '//'", only printing) : stdpp_scope.
Notation "Γ '--------------------------------------' □ Q" :=
  (envs_entails (Envs Γ Enil _) Q%I)
  (at level 1, Q at level 200, left associativity,
  format "Γ '--------------------------------------' □ '//' Q '//'", only printing)  : stdpp_scope.
Notation "'--------------------------------------' ∗ Q" := (envs_entails (Envs Enil Enil _) Q%I)
  (at level 1, Q at level 200, format "'--------------------------------------' ∗ '//' Q '//'", only printing) : stdpp_scope.

view this post on Zulip Ralf Jung (Jul 27 2021 at 16:11):

also I copied that to my minimal examples as well and the issue does not arise there

view this post on Zulip Ralf Jung (Jul 27 2021 at 16:15):

declaring the notation like this instead

Reserved Notation "|={ E }=> Q"
  (at level 99, E at level 50, Q at level 200,
   format "'[hv' |={ E }=>  '/' Q ']'").

fixes the problem. now I guess I have to do this for all the dozen notations we have that look roughly like this...

view this post on Zulip Ralf Jung (Jul 27 2021 at 16:20):

without the hv it also works

view this post on Zulip Hugo Herbelin (Jul 27 2021 at 19:14):

Thanks for reporting. There is indeed a disruptive vertical box present in the goal printer (so that hypotheses are vertically displayed). If you have a version of Coq sources around, you can try to apply the following patch:

--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -470,7 +470,7 @@ let pr_goal ?(diffs=false) ?og_s g_s =
     else
       pr_context_of env sigma ++ cut () ++
         str "============================" ++ cut ()  ++
-        pr_letype_env ~goal_concl_style:true env sigma concl
+        hov 2 (pr_letype_env ~goal_concl_style:true env sigma concl)
   in
   str "  " ++ v 0 goal

which should solve your problem w/o having to modify "|={ E }=> Q". I'll submit a PR anyway.

view this post on Zulip Ralf Jung (Jul 27 2021 at 20:39):

@Hugo Herbelin thanks for tracking it down! I was unable to reproduce outside iris

view this post on Zulip Ralf Jung (Jul 27 2021 at 20:40):

we probably want a fix that works with current versions of Coq, so we'll stick with adding '[' now, but good to know it will be fixed in the future :)

view this post on Zulip Ralf Jung (Jul 27 2021 at 21:45):

while we are at it, @Hugo Herbelin maybe you can help me with a printing question... we have things that print like this right now:

|={  N}=>  one_shot_inv γ l
               WP match: InjRV #m' with
                     InjL <> => assert: #false
                   | InjR "m" => assert: #m = "m"
                   end
                {{ _, True }}

I would like them to print like this:

|={  N}=>  one_shot_inv γ l
   WP match: InjRV #m' with
         InjL <> => assert: #false
       | InjR "m" => assert: #m = "m"
       end
    {{ _, True }}

IOW, I'd like it to use the line after |={⊤ ∖ ↑N}=> and then start the following lines indented by 2... but instead it indents by enough to visually align things with the previous line.
I thought I could achieve the desired effect with this format:

Reserved Notation "|={ E }=> Q"
  (at level 99, E at level 50, Q at level 200,
   format "'[  ' |={ E }=>  Q ']'").

but that doesn't seem to do it. It still treats Q as a block somehow, or so.

view this post on Zulip Ralf Jung (Jul 27 2021 at 21:53):

oh interesting, it seems to be related to the default format for

view this post on Zulip Ralf Jung (Jul 27 2021 at 21:53):

we defined this as just

Reserved Notation "P ∗ Q" (at level 80, right associativity).

when I made it

Reserved Notation "P ∗ Q" (at level 80, right associativity, format "P  ∗  '/' Q").

that yielded the desired result.
Cc @Robbert Krebbers FYI^

view this post on Zulip Ralf Jung (Jul 27 2021 at 22:17):

ah, but that leads to ugly printing elsewhere

    <<<  x : val, l  x 
     l  x 
     l  x 
     l  x 
     l  x 
     l  x >>>
       code @ 
     <<<  y : val, l  y, RET #() >>>

this might be the same bug as above, but this time I havent yet found a way to work around it

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

ah I can improve the <<< notation

view this post on Zulip Paolo Giarrusso (Jul 28 2021 at 03:57):

The two copies of the sep. conjunction notation seem identical? Paste error?

view this post on Zulip Ralf Jung (Jul 28 2021 at 08:09):

oops fixed

view this post on Zulip Ralf Jung (Jul 28 2021 at 08:10):

I had to add some more boxes in places but now it renders nicely


Last updated: Oct 13 2024 at 01:02 UTC