search

abella-prover / abella

An interactive theorem prover based on lambda-tree syntax
https://abella-prover.org/
GNU General Public License v3.0
89 stars 18 forks source link

Improved control over subgoal display #44

Closed lambdacalculator closed 8 years ago

lambdacalculator commented 8 years ago

This is a feature request (and an incidental bug report).

Andrew Gacek graciously added nested subgoal numbering and the subgoals flag at my request when I was working on some large developments, but after continuing to work on large developments, I find myself wanting an additional axis of control: I would also like to be able to set a maximum number of subgoals (at any level) that are displayed at one time. The motivation is that the ideal number of subgoals to display is often independent of the nesting level but dependent on one's display size, and with predicates defined by dozens of clauses, the display often must either show no subgoals or an overwhelming number of them, to the point that the hypotheses and goal have long scrolled away.

Also, I would like to request that when using a non-infinite value of the subgoals flag, the message reporting the number of subgoals remaining should be broken out by how many subgoals are remaining at each level. This information is often a better summary of one's position in the proof than just the total number of subgoals remaining.

Finally, if these features are implemented, I would recommend additionally taking a careful look at the code that generates subgoal numbers. The other day, I came across a small bug in the middle of a big proof that involved two successive subgoals being given the same number. I didn't make a ticket for it because I didn't have the time to isolate the problem and extract a small portion of my large development that illustrated it at the time, and now I can't find it again, although I'm sure it was there. This was the only time I've seen it happen, however, so it seems quite rare. I'm passing along this information here just as a head's up, since, if you end up implementing my suggested features, then you will at least be looking at this code, and if you pay a little extra attention to the invariants there, you might spot the problem.

chaudhuri commented 8 years ago

Broken up into #47, #48, #49.