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



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
subgoals.
- 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.
- 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.

Please keep in mind that this is not a plea to change anything. I'm
perfectly happy with the Output panel with the "Proof state" checkbock
ticked. I just wanted to give some insight into my workflow and maybe
provoke further input from people working similarly or differently to
give the developers more data to work with.

On Mon, Jan 4, 2016 at 7:20 PM, C. Diekmann <diekmann at in.tum.de> wrote:
> 2016-01-03 22:51 GMT+01:00 Makarius <makarius at sketis.net>:
>> On Sun, 3 Jan 2016, C. Diekmann wrote:
>>
>>> when I first started RC0, the default setting was quite confusing for me.
>>>
>>> I moved the current line cursor to a lemma statement.
>>> What I observed:
>>>  The bottom buffer was set to output. It displays nothing
>>>  The right buffer shows the Documentation panel.
>>>
>>> What I expected:
>>>  The proof state is displayed somewhere.
>>>
>>> The proof state is only visible when I select the state panel (as
>>> documented).
>>
>>
>> There are at least these ways to see the proof state:
>>
>>   (1) Output panel with "Proof state" checkbox ticked (off by default)
>>
>>   (2) State panel, after opening it in a standard way (according to the
>>      explanations in the jEdit or Isabelle/jEdit manuals, so
>>      Documentation *is* important, although not updated yet).
>>
>> These variants roughly correspond to the "2-buffer model" versus "3-buffer
>> model" of ancient Proof General times. It should be rather painless to
>> switch back an forth between these modes, for people who care about that. I
>> tend to use only (2) these days, and also explain it like that to new users.
>
> It is painless. I can confirm that ;-)
> I just documented why I was baffled on the first start. Maybe I still
> live in the apply-style world.
>
>>> This might be confusing for new-comers.
>>
>>
>> Why?  Proof state is only secondary in Isar.  It is possible to give several
>> hours of Isabelle introduction without ever showing State (and Output).  It
>> depends a bit on the topic and the target audience, and on the mindset of
>> the presenter how it is all done.
>>
>> I normally show first the main text area, then its popups, then other
>> things.  Eventually also Output, State, Theories.
>
> Maybe I also need such an introduction. I'm using Isabelle for some
> years now and learned many new things when I attended one of your
> short introduction talks. In particular, the trend to move away from
> `declare[[everything]]` and get the result in the output buffer
> towards ctrl+hover everything. Thanks.
>
>>> Maybe it is a good idea to distribute Isabelle with a simple GUI setup.
>>
>>
>> That was actually the intention of the arrangement of Isabelle2016-RC0. What
>> can be simplified further?
>>
>> I still need to update the Isabelle/jEdit manual in this respect, although I
>> have the impression that most users avoid manuals as much as possible.
>>
>> In addition there could be a nice introductory video.  It is occasionally
>> interesting to see what others have done, and what they find important to
>> tell, e.g. https://www.youtube.com/watch?v=QYbAmRY1C5A
>
> Actually, I did not get the intention behind the GUI until now.
> Probably there should be a "what is new and fancy in Isabelle2016"
> video. For technical details, I still prefer the written
> documentation.
>
> Best Regards,
>   Cornelius
>

Attachment: isabelle_2015.png
Description: PNG image



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