Re: [isabelle] Isabelle2016-RC0 - default output buffers

On Thu, 7 Jan 2016, Julian Brunner wrote:

My thoughts on the subject:

- Interactively viewing the proof state is important to me even though
I never write apply-style proofs. When faced with a proof obligation,
I like to collect the facts that I think will be relevant with
'using'. This allows me to stare at both the facts and the goal
simultaneously in the proof state, getting a better grasp on how to
prove the goal. Without the proof state, I would have to restate the
facts explicitly in order to view them in close proximity to the goal
statement and relieving me of the mental effort of keeping them all in
my mind. It also allows me to play around with the facts and the goal
in order to get a better idea of the proof. Of course, once found, I
may still want to clean up the proof to make it readable without
having access to the proof state.
- The proof state is also useful when dealing with complex induction
rules, relieving me of the mental effort of instantiating the
induction rule in my mind and presenting me with nicely formatted
- Of course, these points do not really apply to educational examples
where an experienced user already knows what the proof state is going
to be at each point of the proof, as well as which tools will be able
to solve which goals. However, they do apply to inexperienced users as
well as experienced users working on complex proofs.

These are classic observations about proof state output. There is nothing to add at the moment, what has not been said in the last 15 years.

- I prefer the 2-buffer model as it takes up less space on my screen
without forcing me to switch between two different panels to get
various kinds of feedback from the system. It allows me to work with
two theories (vertical split), the Theories panel and the Output panel
on a single screen (see attached screenshot). When using the 3-buffer
model, at most one of the feedback buffers actually provides
information most of the time, with the other one just wasting space.
However, since it's not always the same feedback buffer that is
important, I need to keep both of them open anyways. This problem is
made worse by the fact that these panels cannot both be docked at the
bottom by default (since these terms can become large, I prefer to
have them displayed in a wide rather than a tall buffer).
- I prefer touching my mouse as little as possible as I am a fast
typist and keeping my hands on the keyboard is usually much more
efficient. I feel like hovering the mouse over text in order to get
interactive feedback would slow me down significantly.

Fine. It should be trivial to use that model. Just a few clicks to change the defaults. (Unless you have counter examples on that.)

The new model with separate Output vs. State was in the pipeline for many years. There were various reasons why it emerged for Isabelle2016, based on feedback by power users and observations of new users in the past few years.

I have already learned that *any* change in user interface always produces resistance and reluctance on the side of users who have got used to a different mode of operation. This makes it hard to work out if there are genuine problems remaining, or just more time required to get used to it.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.