Email Gateway (Aug 22 2022 at 12:10): Email Gateway (Aug 22 2022 at 12:10):From: "C. Diekmann" <diekmann@in.tum.de>
Hi,
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). This might be confusing for new-comers. In addition, my
proof state is usually huge, but by default, the right panel is very
small.
Splitting state and output may be a good idea for power users with
large displays. On my laptop with only one fullHD display, I just
can't find a satisfying setting. Maybe it is a good idea to distribute
Isabelle with a simple GUI setup. Power users can still change the
defaults. This would mean that by default, the proof state is sent to
the output panel.
What do other users think?
Best Regards,
Cornelius
Email Gateway (Aug 22 2022 at 12:22):From: Makarius <makarius@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.
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.
Unguided new-comers first see the main text buffer and the Documentation
panel -- the latter now starts the clickable "Examples". We probably also
need a guide to the remaining documentation -- maybe another example
theory that uses the new @{doc} antiquotation.
In addition, my proof state is usually huge, but by default, the right
panel is very small.Splitting state and output may be a good idea for power users with large
displays. On my laptop with only one fullHD display, I just can't find a
satisfying setting.
I've just checked again with a conventional 16x9 Full-HD 17" Laptop from
2013, using the default 18px font for the main text area. This
immediately gives at least these options:
(1) Main text is restricted to old-school 80 chars per line, and the
right docking area (with State panel) is extended into the middle of
the main window.
Result: almost 50% screen size for State.
(2) Main text area uses extended line length of 100 chars, and the right
docking area is extended to 30-40% of main window size.
Result: approx. 30-40% screen size for State, or approx. 50% if the
output font scale is set to 85% (this can be done persistently with
the Isabelle plugin option "Font Scale").
Younger people may also try smaller fonts for the main text and/or output.
It is also possible to make a floating instance of State, and put it on a
separate physical screen. That is an investment of 100-200 EUR for
hardware, and some desk space.
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
Makarius
Email Gateway (Aug 22 2022 at 12:23):From: "C. Diekmann" <diekmann@in.tum.de>
2016-01-03 22:51 GMT+01:00 Makarius <makarius@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
Email Gateway (Aug 22 2022 at 12:27):From: Julian Brunner <julianbrunner@gmail.com>
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.
isabelle_2015.png
Email Gateway (Aug 22 2022 at 12:27):From: Tobias Nipkow <nipkow@in.tum.de>
On 03/01/2016 17:38, C. Diekmann wrote:
Hi,
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). This might be confusing for new-comers.> In addition, my
proof state is usually huge, but by default, the right panel is very
small.Splitting state and output may be a good idea for power users with
large displays. On my laptop with only one fullHD display, I just
can't find a satisfying setting. Maybe it is a good idea to distribute
Isabelle with a simple GUI setup. Power users can still change the
defaults. This would mean that by default, the proof state is sent to
the output panel.What do other users think?
I voiced the same concern when the new default was introduced.
Tobias
Best Regards,
Cornelius2016-01-01 20:17 GMT+01:00 Makarius <makarius@sketis.net>:
Dear Isabelle users,
the coming Isabelle2016 release is scheduled for February 2016, after the
next big Java 8 update by Oracle in January and some weeks before the
deadline of ITP 2016.To get started with systematic testing there is now the relatively early
http://isabelle.in.tum.de/website-Isabelle2016-RC0 (corresponding to
Isabelle/e18444532fce and AFP/c62777f3e932).The website, NEWS, ANNOUNCE etc. are already mostly up-to-date. Some
documentation is still lagging behind, notably the Isabelle/jEdit manual.
There are further fine points still to be sorted out.When discussing problems, observations, suggustions, etc. the mail subject
line should be changed to something meaningful (but the release candidate
number still given in the message body).As usual it is important to keep general laws of causality in mind: release
candidates may still change, but the final release is final. Although this
is tautological, in the past few releases we've often had complaints right
after final lift-off, when it was too late.So the best time to start testing is now.
Makarius
Email Gateway (Aug 22 2022 at 12:27):From: Makarius <makarius@sketis.net>
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
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.
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.
Makarius
Email Gateway (Aug 22 2022 at 12:27):From: Makarius <makarius@sketis.net>
Can you quote a changeset and mailing list message on that?
The State output has changed many times in the past few months. I have
incorporated all observations and feedback into Isabelle2016-RC0 as far as
I can tell.
If anything has been overlooked, I need concrete information on that.
Makarius
Email Gateway (Aug 22 2022 at 12:28):From: Tobias Nipkow <nipkow@in.tum.de>
On 08/01/2016 16:36, Makarius wrote:
On Thu, 7 Jan 2016, Tobias Nipkow wrote:
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). This might be confusing for new-comers.> In addition, my
proof state is usually huge, but by default, the right panel is very
small.Splitting state and output may be a good idea for power users with
large displays. On my laptop with only one fullHD display, I just
can't find a satisfying setting. Maybe it is a good idea to distribute
Isabelle with a simple GUI setup. Power users can still change the
defaults. This would mean that by default, the proof state is sent to
the output panel.What do other users think?
I voiced the same concern when the new default was introduced.
Can you quote a changeset and mailing list message on that?
See
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2015-November/006420.html
Tobias
The State output has changed many times in the past few months. I have
incorporated all observations and feedback into Isabelle2016-RC0 as far as I can
tell.If anything has been overlooked, I need concrete information on that.
Makarius
smime.p7s
Email Gateway (Aug 22 2022 at 12:28):From: Makarius <makarius@sketis.net>
That is a rather old thread. I don't see any connection to the way it
works in Isabelle2016-RC0.
Of course you can always re-open a new discussion.
Makarius
Email Gateway (Aug 22 2022 at 12:29):From: Tobias Nipkow <nipkow@in.tum.de>
On 09/01/2016 13:21, Makarius wrote:
On Sat, 9 Jan 2016, Tobias Nipkow wrote:
Can you quote a changeset and mailing list message on that?
See
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2015-November/006420.htmlThat is a rather old thread. I don't see any connection to the way it works in
Isabelle2016-RC0.
Both Cornelius and I refer to the fact that the proof state is not displayed by
default in the output window.
Tobias
Of course you can always re-open a new discussion.
Makarius
Email Gateway (Aug 22 2022 at 12:29):From: Lawrence Paulson <lp15@cam.ac.uk>
Personally, I have no problem with the change itself. The new way is cleaner, avoiding mixing error messages with the state output. But it could be disconcerting when encountered for the first time, so we need to advertise it clearly. I have completely switched to the State window and only display the Output window very exceptionally. Other people will do things differently.
Larry
Email Gateway (Aug 22 2022 at 12:30):From: Makarius <makarius@sketis.net>
The key difference to the version in November 2015:
* Output has a button to enable "Proof state"
* State has a button to disable "Auto update"
Thus it is trivial to switch certain modes of operation on the fly.
The State buffer is conceptually cleaner and has many other advantages.
The main disadvantage: users need to change old habits, as usual.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC