Repository navigation
Using PG/xml, C-c C-p no longer shows the context for the current goal #233
Description
@psteckler I have a context and goal that looks like this:
1 subgoal
subgoal 1 (ID 37):
C : Category
objs : obj_idx → C
arrmap : M.t (∃ x y : obj_idx, objs x ~{ C }~> objs y)
dom, i, j : obj_idx
from, to : ∃ hs : list arr_idx, ReifiedArrow objs arrmap i j hs
cod : obj_idx
x : list arr_idx
p : ReifiedArrow objs arrmap dom cod x
―――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――
∃ ks : list arr_idx, ReifiedArrow objs arrmap dom cod ks
When I use C-c C-p now to refresh the display, or after hitting the electric terminator, all that I see in the *goals* buffer is:
―――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――
∃ ks : list arr_idx, ReifiedArrow objs arrmap dom cod ks
Activity
psteckler commentedon Mar 1, 2018
I can verify that
C-c C-pissues aGoalrequest to coqtop, which sends back the current goal.Do you mean that the hypotheses have scrolled out of view, or are they missing entirely?
jwiegley commentedon Mar 1, 2018
The Hypotheses are being scrolled out of view. I can scroll them back, but it requires moving point into the Goals window to do so.
masterbranch keeps as much in view as possible.psteckler commentedon Mar 1, 2018
Got it, I'll look at that.
psteckler commentedon Mar 1, 2018
PG/xml is making some attempt to scroll the goals buffer on
C-c C-p, it's basically the same code as inmaster.In an example I tried, with a large context, the goal scrolled slightly below the buffer separator, rather than right at the bottom, as in
master. But that seems opposite to what you saw. I'll see if I can fine-tune the behavior.Matafou commentedon Mar 1, 2018
Indeed the best heuristic I found for that is to show as much as possible of the goal's conclusion.
Then:
coq-prefer-top-of-conclusion.@psteckler this is implemented in
coq-show-first-goalwhich is called in a hook.Matafou commentedon Mar 1, 2018
Please try setting
coq-prefer-top-of-conclusiontot.psteckler commentedon Mar 1, 2018
It's called explicitly in PG/xml, renamed to
coq-goals--show-first-goal.psteckler commentedon Mar 1, 2018
In
coq/coq-goals.el, incoq-goals--show-first-goal, if I change the line(recenter -1)to(recenter -2), the conclusion appears with just a small gap above the separator. It looks nice.@jwiegley Can you try making that change, recompiling. If it looks good, I'll submit a PR with the change.
jwiegley commentedon Mar 1, 2018
psteckler commentedon Mar 2, 2018
If that's set to
t, I see the behavior reported by @jwiegley, which is different than what happens inmaster. Investigating ...psteckler commentedon Mar 2, 2018
I think that PG/xml may be doing the right thing in the case that
coq-prefer-top-of-conclusionist.If I understand the code here, it says that if the separator is not visible, then put the point at the separator, then put the point 0 lines from the top of the window -- which is what you showed above.
For PG in
master, the goal display must be already showing the separator, soC-c C-pdoesn't do thatrecenter.I think you may get what you want by setting
coq-prefer-top-of-conclusiontonil. That will put the bottom of the conclusion at the bottom of the window. Currently, that's done by moving the point to the bottom of the first goal, then running(recenter (- 1)). I think it looks a little better if you run(recenter -2).jwiegley commentedon Mar 2, 2018
So, the reason I don't have it set to
nilis what happens where there are multiple sub-goals: it scrolls the goal you want to see out of view. It's really themasterbranch's behavior whencoq-prefer-top-of-conclusionistthat I want to keep.Matafou commentedon Mar 3, 2018
@psteckler in principle if we do not see the goal separator it means that there is not enough room to see hypothesis. In @jwiegley example the goal is a one liner so this code is not triggered at all. This code is meant to maximize the display of the current goal with a priority on the conclusion. Coq-prefer is only to decide if one prefer the top of the conclusion or its end.
But all this is supposed to be executed once the buffer is scrolled to see the end of the 1st goal. Maybe this is the pb in pgxml?
psteckler commentedon Mar 3, 2018
Yes, in
asyncthat invariant is broken before callingshow-first-goal. I'll have to investigate why.psteckler commentedon Mar 5, 2018
Created #342. Please see whether this fixes the issue.