Using PG/xml, C-c C-p no longer shows the context for the current goal

[jwiegley]

@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

[psteckler]

I can verify that C-c C-p issues a Goal request 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]

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. master branch keeps as much in view as possible.

[psteckler]

Got it, I'll look at that.

[psteckler]

PG/xml is making some attempt to scroll the goals buffer on C-c C-p, it's basically the same code as in master.

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]

Indeed the best heuristic I found for that is to show as much as possible of the goal's conclusion.
Then:

1. If it does not fit in the window I tend to prefer to see the beginning of the conclusion but some people prefer to see the end. This is ruled by variable coq-prefer-top-of-conclusion.
2. if there is room, show as much hypothesis as possible.

@psteckler this is implemented in coq-show-first-goal which is called in a hook.

[Matafou]

Please try setting coq-prefer-top-of-conclusion to t.

[psteckler]

coq-show-first-goal which is called in a hook.

It's called explicitly in PG/xml, renamed to coq-goals--show-first-goal.

[psteckler]

In coq/coq-goals.el, in coq-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]

Please try setting coq-prefer-top-of-conclusion to t.

I do have this set to `t`.

[psteckler]

coq-prefer-top-of-conclusion

If that's set to t, I see the behavior reported by @jwiegley, which is different than what happens in master. Investigating ...

[psteckler]

I think that PG/xml may be doing the right thing in the case that coq-prefer-top-of-conclusion is t.

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, so C-c C-p doesn't do that recenter.

I think you may get what you want by setting coq-prefer-top-of-conclusion to nil. 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]

So, the reason I don't have it set to nil is what happens where there are multiple sub-goals: it scrolls the goal you want to see out of view. It's really the master branch's behavior when coq-prefer-top-of-conclusion is t that I want to keep.

[Matafou]

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

But all this is supposed to be executed once the buffer is scrolled to see the end of the 1st goal

Yes, in async that invariant is broken before calling show-first-goal. I'll have to investigate why.