The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 06/17/2016 10:26 PM, Clément Pit--Claudel wrote:
> On 2016-06-17 19:26, Jonathan Leivent wrote:
> > Here's a priority order of what I'd like to see without scrolling, if the 
> > goal window is big enough:
> > 1. all of the goals in focus, with their hyps
> > 2. all of the current goal, and as many of the next goals as can fit 
> > completely, but at least all conclusions
> > 3. the whole current goal's conclusion, with as many hyps above it as fit
> I think 1 + 3 is the current behaviour (IIRC)

3 is the current behavior when room is limited to <= just the current 
goal, which is why I put it last.  In 1 and 2, if room permits, I'd like 
to see complete goals with hyps, not just their conclusions.

For example, when doing induction, the first subgoal will usually be the 
base case, which is rarely where the question of "did I use the right 
kind of induction over the right hyps?" is answerable.  Seeing the hyps 
of the other subgoals would help.  Right now, whenever I do a 
questionable induction, I manually show the other subgoals (^C^A^S n, 
one at a time) to check them out.

Another is when about to use a goal selector other than 1: (and soon 
we'll have a richer set of goal selectors).

Another is when there are evars shared across multiple goals, such that 
how those goals depend (or not) on the evars impacts which goal I'll try 
to solve next.

There's probably a bunch of ways to try to get more useful info into the 
goals window.  I mentioned hide/show, with increasing hiding done as 
space runs out.  Maybe another would be multiple goal windows.  While 
proving, I rarely need a full vertical window for the script, but often 
need more than a full vertical window for the goals - so if I could see 
other goals in other windows, that would be making better use of screen 
real estate than now.  Usually, I have 2 screens to use - but currently 
that doesn't help me do anything but spread things out horizontally.  
Unfortunately, neither of those screens can do a portrait/landscape flip.

-- Jonathan