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
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.
@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.
also I copied that to my minimal examples as well and the issue does not arise there
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...
without the hv
it also works
Thanks for reporting. There is indeed a disruptive v
ertical 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.
@Hugo Herbelin thanks for tracking it down! I was unable to reproduce outside iris
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 :)
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.
oh interesting, it seems to be related to the default format for ∗
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^
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
ah I can improve the <<<
notation
The two copies of the sep. conjunction notation seem identical? Paste error?
oops fixed
I had to add some more boxes in places but now it renders nicely
Last updated: Oct 13 2024 at 01:02 UTC