Email Gateway (Aug 19 2022 at 09:38): Email Gateway (Aug 19 2022 at 09:38):From: Alfio Martini <alfio.martini@acm.org>
Dear Isabelle Users,
Maybe it is just me, but I still get confused by the new error messages in
Isabelle 2013. Of course, it is already
a big improvement over simply "failed to finish proof" from Isabelle 2012.
For instance, the success of establishing a "have" or a "show" is usually
show in the output window
with a message like "have fact" " show fact ... successful attempt to
solve goal by exported rule"
Now, when there´s a failure, the error message is still prefixed in the
output window by the
very messages we get when we are successful, as mentioned above. Besides in
the error case, the
output window also show after the error message that there are no subgoals
(?).
I attach two images to make my point clearer.
In this particular example, if the error message was not prefixed by
"Successful attempt ...", I think it would
be much better.
Is my confusion justified?
Best!
jedit-proof-sucess.PNG
jedit-proof-failure.PNG
Email Gateway (Aug 19 2022 at 09:41):From: Makarius <makarius@sketis.net>
On Mon, 21 Jan 2013, Alfio Martini wrote:
Maybe it is just me, but I still get confused by the new error messages
in Isabelle 2013. Of course, it is already a big improvement over simply
"failed to finish proof" from Isabelle 2012.
Is my confusion justified?
There were no reactions so far, so maybe nobody else has tried it yet.
This refinement of error messages was the result of myself using the
system over 1-2 weeks to prepare some Isabelle tutorial last October. At
some point I got tired of looking up the Output again and again. Instead
it is now possible to do quite a lot of proofs right there in the text,
without peeking at the goal state. You just hover over the red squiggles
of the failed proof methods and immediately see what happened. This is
escpecially relevant for structured Isar proofs.
Output and goal states are not fully obsolete yet, but it is one more
step to overcome them.
For instance, the success of establishing a "have" or a "show" is usually
show in the output window
with a message like "have fact" " show fact ... successful attempt to
solve goal by exported rule"Now, when there´s a failure, the error message is still prefixed in the
output window by the
very messages we get when we are successful, as mentioned above. Besides in
the error case, the
output window also show after the error message that there are no subgoals
(?).I attach two images to make my point clearer.
In this particular example, if the error message was not prefixed by
"Successful attempt ...", I think it would
be much better.
There are several things being mixed up in the all-inclusive Output
window. The "Successful attempt" is just a preview of the attempt to
apply the command, stemming from old TTY-times. It is more and more
getting in the way.
Also note that there is some non-determinism stemming from the fork of
'by' steps that is now enabled by default, cf. NEWS. That sometimes leads
to nice top-down checking of proof outlines, where the system jumps over
failed justification. Sometimes this does not work, due to bad timing,
and the proof text produces a lot of structural errors about displaced qed
after a failed sub-proof.
There might be also some genuine problems in the RC1 snapshot left. Just
the week before making it, I had to rework the error reporting once more
to avoid duplication of errors from one 'by' step to another 'by' step.
I will myself look again if it is as right as possible right now, unless
someone else points directly to remaining drop-outs.
Makarius
Email Gateway (Aug 19 2022 at 09:41):From: Alfio Martini <alfio.martini@acm.org>
Hi Makarius.
Instead it is now possible to do quite a lot of proofs right there in the
hover-error-message.PNG
Email Gateway (Aug 19 2022 at 09:41):From: Peter Lammich <lammich@in.tum.de>
This is great. I did not know that. I am probably being very naive here (to
put it mildly), but what appears in the
window that pops up when you hover over the red squiggles is what I would
expect to appear
in the output window as well (see image attached) .
I agree with Alfio. When I write proofs, I usually do this
incrementally. If, at some point, I type eg
have foo by auto
and the proof method fails unexpectedly, I would like to immediately see
why, without moving my arm from the keyboard to the mouse, hover the
mouse over the text and wait for the popup.
Still, this feature is better than what we have in the 2012-version,
where you had to go back to the "by" and change it to an apply, just in
order to see the remaining subgoals in the output buffer.
Best,
Peter
Best!
On Fri, Jan 25, 2013 at 2:22 PM, Makarius <makarius@sketis.net> wrote:On Mon, 21 Jan 2013, Alfio Martini wrote:
Maybe it is just me, but I still get confused by the new error messages
in Isabelle 2013. Of course, it is already a big improvement over simply
"failed to finish proof" from Isabelle 2012.
Is my confusion justified?
>There were no reactions so far, so maybe nobody else has tried it yet.
This refinement of error messages was the result of myself using the
system over 1-2 weeks to prepare some Isabelle tutorial last October. At
some point I got tired of looking up the Output again and again. Instead
it is now possible to do quite a lot of proofs right there in the text,
without peeking at the goal state. You just hover over the red squiggles
of the failed proof methods and immediately see what happened. This is
escpecially relevant for structured Isar proofs.Output and goal states are not fully obsolete yet, but it is one more step
to overcome them.For instance, the success of establishing a "have" or a "show" is usually
show in the output window
with a message like "have fact" " show fact ... successful attempt to
solve goal by exported rule"Now, when there愀 a failure, the error message is still prefixed in the
output window by the
very messages we get when we are successful, as mentioned above. Besides
in
the error case, the
output window also show after the error message that there are no subgoals
(?).I attach two images to make my point clearer.
In this particular example, if the error message was not prefixed by
"Successful attempt ...", I think it would
be much better.
There are several things being mixed up in the all-inclusive Output
window. The "Successful attempt" is just a preview of the attempt to apply
the command, stemming from old TTY-times. It is more and more getting in
the way.Also note that there is some non-determinism stemming from the fork of
'by' steps that is now enabled by default, cf. NEWS. That sometimes leads
to nice top-down checking of proof outlines, where the system jumps over
failed justification. Sometimes this does not work, due to bad timing, and
the proof text produces a lot of structural errors about displaced qed
after a failed sub-proof.There might be also some genuine problems in the RC1 snapshot left. Just
the week before making it, I had to rework the error reporting once more to
avoid duplication of errors from one 'by' step to another 'by' step.I will myself look again if it is as right as possible right now, unless
someone else points directly to remaining drop-outs.Makarius
Email Gateway (Aug 19 2022 at 09:42):From: Makarius <makarius@sketis.net>
The screenshot does not show the position of the cursor (or "caret" in
Java terminology). Where is it actually? The output window follows that,
in reminiscence of old-style TTY interaction where you have a single
focus.
Makarius
Email Gateway (Aug 19 2022 at 09:42):From: Alfio Martini <alfio.martini@acm.org>
Hi Makarius,
I have sent this already in a message previous to this one. The question is
simple:
I (as many other Isabelle users, I suppose) depend very much on the output
window to work with
Isabelle even though I work essentially with Isar structured proofs. The
hover-over-the-scribbles
feature is nice, but the output window is better and faster.
The problem is that, in case of a problem in establishing a fact or a
pending goal,
the output window is now displaying messages
that show both success and failure (jedit-proof-failure) of applying a
given proof method , and
I think this should be avoided at all costs. If it is not possible in
Isabelle 2013, then maybe in Isabelle
2014. In the case of the error message, the output window should display
only
the message that appear in the image hover-error message, and not an
ambiguous message as
shown in the jedit-proof-failure image. See attachments.
best!
jedit-proof-failure.PNG
hover-error-message.PNG
jedit-proof-sucess.PNG
Email Gateway (Aug 19 2022 at 09:43):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 1/28/2013 10:19 AM, Alfio Martini wrote:
I have sent this already in a message previous to this one. The question is
simple:
I (as many other Isabelle users, I suppose) depend very much on the output
window to work with
Isabelle even though I work essentially with Isar structured proofs. The
hover-over-the-scribbles
feature is nice, but the output window is better and faster.
I would hate to see the output panel ever go away for proof goals. If
anything, I'd like to see information generated there when I click on a
line for something like "definition", "consts", "notation",
"abbreviation", and get any useful information that the prover engine is
using that gets hidden. I have these commands in:
declare[[show_brackets=true]] declare[[show_types=true]]
declare[[names_unique=true]] declare[[show_consts=true]]
There ends up being a lot of information for a proof step, and the
output panel allows me to fix the location and size of the window for
how I prefer to view that information.
I also get an error window popping up when I'm typing something new
because my syntax isn't right because I haven't finished it all.
I set "Editor Chart Delay" to 10, but these windows keep occasionally
popping up. If I keep typing, it rings an error bell for each keystroke,
and the window is visually in the way.
There's a lot of visual information that automatically gets generated,
like an error icon in the gutter on the right, or the vertical bar going
purple on the left, and the squiggly lines of different colors, and all
that is good.
However, I would say that windows popping up to notify me of something
on a frequent basis is overall a bad thing. I say more below.
Makarius wrote:
The screenshot does not show the position of the cursor (or "caret" in
Java terminology). Where is it actually? The output window follows that,
in reminiscence of old-style TTY interaction where you have a single focus.
I wouldn't put the output panel in the category of being old-style. It's
a left, right, or bottom dockable window that's part of a modern, GUI
editor. Being able to look at both the edit buffer and the output panel
at the same time at least gives it a dual focus ability.
It comes down to personal preference, but I put a lot of effort into
getting my windows all set up. With jEdit, I use a three panel view:
edit buffer, left panel, and bottom panel.
It all looks nice. The popup windows are sort of ugly.
And when a window pops up I wasn't expecting that tries to help me out,
when I don't want any help, because I don't care about the error, I
don't really like that, and I make sure I keep a proper perspective on
how powerful the Isabelle software is.
If I hover over something to intentionally get the popup window, I like
that, especially when it gives me useful information.
The popup windows are a good addition, but I also like to control where
my main "information" windows are, which, with jEdit, is docking them in
a fixed location I want them to be.
Regards,
GB
Email Gateway (Aug 19 2022 at 09:43):From: Makarius <makarius@sketis.net>
On Mon, 28 Jan 2013, Gottfried Barrow wrote:
I have these commands in:
declare[[show_brackets=true]] declare[[show_types=true]]
declare[[names_unique=true]] declare[[show_consts=true]]
I have worked very hard to eliminate the need for these in most practical
situations. You don't need this information all the time, only when
something is wrong. Then you use CTRL-hover etc. to look what is there.
There ends up being a lot of information for a proof step, and the
output panel allows me to fix the location and size of the window for
how I prefer to view that information.
There is an option for "tooltip margin" to control the window width in a
soft manner. The location is determined by the location of the
information in the source text. This is a very important principle of the
Prover IDE, and the direction where it is moving for several years
already.
I also get an error window popping up when I'm typing something new
because my syntax isn't right because I haven't finished it all.
This sounds more like a variation of platform-specific focus handling.
Error message popups only show up for red squiggles in the text. Maybe
you have the mouse pointer in the way, or maybe there is some Windows snag
behind it (I am more used to Linux and Mac OS X snags in that respect).
I set "Editor Chart Delay" to 10, but these windows keep occasionally
popping up. If I keep typing, it rings an error bell for each keystroke,
and the window is visually in the way.
See the option tooltip for what this is for. Tooltip timing is determined
by certain Java/Swing properties, but I don't know exactly which one.
I wouldn't put the output panel in the category of being old-style. It's
a left, right, or bottom dockable window that's part of a modern, GUI
editor. Being able to look at both the edit buffer and the output panel
at the same time at least gives it a dual focus ability.
That is old-school Proof General mode. When developing complex formal
documents you need more than dual (or triple) focus, but it does not work
by putting more windows there. One needs to make the one main window
smarter: the source window.
Makarius
Email Gateway (Aug 19 2022 at 09:43):From: René Neumann <rene.neumann@in.tum.de>
Do I understand this correctly: Eventually, the output panel will
completely be removed and you have to hover the mouse-pointer over
everything to get any information?
Email Gateway (Aug 19 2022 at 09:43):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 1/28/2013 12:56 PM, Makarius wrote:
On Mon, 28 Jan 2013, Gottfried Barrow wrote:
I have these commands in:
declare[[show_brackets=true]] declare[[show_types=true]]
declare[[names_unique=true]] declare[[show_consts=true]]I have worked very hard to eliminate the need for these in most
practical situations. You don't need this information all the time,
only when something is wrong. Then you use CTRL-hover etc. to look
what is there.
Makarius,
But that is your personal preference, which reigns supreme in
influencing your decisions on what features to add or eliminate.
Myself, I greatly appreciate that Isar syntax allows many implicit
meanings, but I currently always want to see explicit typing and
grouping used for the constants and the formulas for a proof step. It's
a happy medium. I don't have to clutter up the code, but I always get to
check the typing and grouping without having to do anything other than
look down at the output panel.
Do do that now, if the output panel is docked at the bottom, I merely
have to shift my eyes down to the bottom of the editor.
I wouldn't put the output panel in the category of being old-style.
It's a left, right, or bottom dockable window that's part of a
modern, GUI editor. Being able to look at both the edit buffer and
the output panel at the same time at least gives it a dual focus
ability.That is old-school Proof General mode. When developing complex formal
documents you need more than dual (or triple) focus, but it does not
work by putting more windows there. One needs to make the one main
window smarter: the source window.
I have decided that this can be categorized under "floating vs. docked
window preference".
Suppose the need was eliminated to display any of the proof step
information in the output panel. I forsee in the future that someone
would make a request like this: "Makarius, you know those different
kinds of popup windows that give us information? Can you make it where
we can choose for them to be either floating or dockable? You might have
an options button which allows us to select or deselect error info,
proof info, term info, etc. "
Here, I use the specific example of Sledgehammer and Nitpick. You have
it now where we can get the output in two different places, the output
panel or by hovering the mouse over the command.
But if I know I always want to see the output, and I want to see the
output as the command is running, then what I want is a panel, docked or
floating, that's specifically displayed for that purpose. I also want it
fixed in size and location.
There's more info to be seen than can be displayed, so I like the jEdit
plugin model. You can display or not display a window for a plugin. You
can dock or not dock a window you display. You can dock a window in 4
different places. That's a lot of options on how to display information.
Old skool with improvements, along with completely new features is
sometimes the best way to go. But that's easy for me to say, and I don't
have to implement it.
Thanks,
GB
Email Gateway (Aug 19 2022 at 09:46):From: Makarius <makarius@sketis.net>
I am still confused about this confusion. Taking the above specification
in isolation, it is already what happens in Isabelle2013-RC2: you see the
error "immediately" in the output of the by command, assuming that window
is open in the old-fashioned manner; it also works Proof General. If you
don't have output open, then pointing at the red squiggles of "auto" gives
the error more quickly.
If this does not work for you, it might be a remaining problem timing
problem, platform-specific window update problem etc.
Makarius
Email Gateway (Aug 19 2022 at 09:46):From: Makarius <makarius@sketis.net>
I've categorized this as "old-style", "old-fashioned", "old-school".
This is one stage before "legacy". After "legacy" comes "discontinued".
The full cycle can take many years.
I am still curious to see how far the approach of augmented editing of
formal sources can be pushed for Isar proof development, leaving TTY
commands and output windows behind. It has been the trajectory of the
Prover IDE for several years already, and we are now approaching the point
where many technical side-conditions are settled, to make more serious
attempts at structured editing support. Isabelle2013 is just one more
step, but not the last one.
Makarius
Email Gateway (Aug 19 2022 at 09:46):From: Makarius <makarius@sketis.net>
It works better if you disable show_types and show_sorts by default.
Isabelle2013 will then add the annotations to all possible positions as
markup to the output, and you can hover over it to see what is there and
what is wrong. If show_types / show_sorts are enabled, you get the old
behaviour of partial printing directly in the text.
The ambition in Isabelle2013 was to eliminate then need for show_types /
show_sorts altogether -- I've got too many complaints about such options
missing in the "menu". Lets see how far it is now from 0.00001 relevance.
Makarius
Email Gateway (Aug 19 2022 at 09:46):From: Makarius <makarius@sketis.net>
On Mon, 28 Jan 2013, Gottfried Barrow wrote:
I have decided that this can be categorized under "floating vs. docked
window preference".
This sounds more like an aspect of the dockable window manager in jEdit.
It is nice for what it does, but could be improved. Unfortunetely, there
are extremely few people now picking up the challenge to make real
improvements there. I can understand that, because the slightest change
in window behaviour causes a lot of worries on all platforms and
look-and-feel themes of Java/Swing.
Here, I use the specific example of Sledgehammer and Nitpick. You have
it now where we can get the output in two different places, the output
panel or by hovering the mouse over the command.But if I know I always want to see the output, and I want to see the
output as the command is running, then what I want is a panel, docked or
floating, that's specifically displayed for that purpose. I also want it
fixed in size and location.
It is merely a technical snag that the tooltip popups are not dynamically
updated, so Output is presently the only way to get incremental output on
the spot as it arrives.
Looking at the bigger picture, the command + output mode of Sledgehammer
and Nitpick is just a historical accident. The long-standing plan is to
provide more direct support for "asynchronous agents" in the Prover IDE to
produce feedback on the text as you write it. Such an agent would have
its own panel somewhere to control it, although the feedback is more
likely to appear around the text itsel, like a spell-checker; or as some
icons or bubbles indicating suggestions to the user.
There's more info to be seen than can be displayed, so I like the jEdit
plugin model. You can display or not display a window for a plugin. You
can dock or not dock a window you display. You can dock a window in 4
different places. That's a lot of options on how to display information.
Note that in jEdit "plugin" is just some Java module loaded in a certain
way. You probably mean "dockable window", the thing that is managed by
the "dockable window manager". The Isabelle plugin provides several
dockable windows: Output, Symbols, Theories etc.
4 different places for docking are nice, but I can imagine much more
sophistication. Someone made an alternative dockable window manager for
jEidt called "MyDoggy", but it now looks unmaintained and outdated. One
could invest more here, but I am certainy not doing it myself.
Old skool with improvements, along with completely new features is
sometimes the best way to go. But that's easy for me to say, and I don't
have to implement it.
There is always a continous ongoing process of improvements. Keywords
like "new" and "feature" are marked as dangerous in my vocabulary, though.
Progress requires clear concepts first and then a long way to get it
through in the implementation, and finally reach users.
Makarius
Email Gateway (Aug 19 2022 at 09:46):From: René Neumann <rene.neumann@in.tum.de>
Am 30.01.2013 14:08, schrieb Makarius:
Do I understand this correctly: Eventually, the output panel will
completely be removed and you have to hover the mouse-pointer over
everything to get any information?I've categorized this as "old-style", "old-fashioned", "old-school".
This is one stage before "legacy". After "legacy" comes "discontinued".
The full cycle can take many years.
I'll take this as a wordy "yes, but will take some time".
I am still curious to see how far the approach of augmented editing of
formal sources can be pushed for Isar proof development, leaving TTY
commands and output windows behind.
Please keep in mind, that the good ol' TTY approach with only one single
point of focus is not overall obsolete: When dealing with a single
proof, one normally only focuses on the lines one is writing. So if
there will be a reasonable replacement for the output window (i.e.
immediate display of messages), this is fine. But having to use the
mouse to get the information is not (even a hotkey for "get message
under cursor" probably will be cumbersome).
Email Gateway (Aug 19 2022 at 09:46):From: Lars Noschinski <noschinl@in.tum.de>
I think Peter's point is that he would not like to work with a version
of Isabelle where you cannot see directly what is happening at the
editing focus. Some of your comments like
| Output and goal states are not fully obsolete yet, but it is one more
| step to overcome them.
can be interpreted as wanting to remove that way of working.
-- Lars
Email Gateway (Aug 19 2022 at 09:47):From: Lars Noschinski <noschinl@in.tum.de>
Actually, I think René Neumann did a good job of explaining what I
wanted to express here.
-- Lars
Email Gateway (Aug 19 2022 at 09:47):From: Lawrence Paulson <lp15@cam.ac.uk>
I would like the output panel to remain, if at all possible. Having to click on something to see the current state is cumbersome, and if I understand your comment, it is only available for errors and not for inspection of an arbitrary intermediate proof state. But that's what I often want to do. Moreover, the pop-up windows are quite small and will typically need resizing.
Larry
Email Gateway (Aug 19 2022 at 09:47):From: Makarius <makarius@sketis.net>
When you say "the editing focus" and "directly" it already has a strong
bias towards the TTY model. Isabelle/jEdit is moving more and more away
from that, as far as it becomes feasible. I am especially interested to
see decent Isar proof editing facilities, without the TTY side-conditions.
This does not mean that the Output panel of Isabelle/jEdit will just
disappear in the next release. There are applications where you do need
free-form output from commands.
There are important special cases though:
(1) proof development, especially structured proof development
(2) feedback from ATPs via sledgehammer etc.
Here I can imagine more direct user interface support than the old TTY
loop.
Makarius
Email Gateway (Aug 19 2022 at 09:48):From: Makarius <makarius@sketis.net>
On Wed, 30 Jan 2013, René Neumann wrote:
Please keep in mind, that the good ol' TTY approach with only one single
point of focus is not overall obsolete: When dealing with a single
proof, one normally only focuses on the lines one is writing.
This is even before Proof General and especially before Isar proofs. Can
you show some of your proofs that you normally do?
I find it very awkward to produce structured proofs with that "good
ol'" TTY model, or the slight variation of it in Proof General.
Isabelle/jEdit of Isabelle2013 is moving a tiny little bit forward, but
still not there to edit proof structure directly, without funny machine
state inspection all the time.
But having to use the mouse to get the information is not (even a hotkey
for "get message under cursor" probably will be cumbersome).
So maybe that is a starting point to get active, and investigate
possibilities of the jEdit platform.
Of course, one would also have to step back, and look conceptually on the
problem what the message under the cursor means, bacause that is not fully
trivial without assuming an understanding of old-style TTY command
boundaries.
Or did you mean a keyboard version of "hover over squiggles"?
Makarius
Email Gateway (Aug 19 2022 at 09:48):From: Makarius <makarius@sketis.net>
Did you try adjusting the various tooltip options in the Plugin Options /
Isabelle panel of jEdit? It is basically a menu, were you can see what is
there, and look at the tooltips to guess what is the purpose.
Makarius
Email Gateway (Aug 19 2022 at 09:48):From: Alfio Martini <alfio.martini@acm.org>
Hi Makarius,
BTW, you can try to set "Parallel Proofs" to 0 (in Plugin Options /
error_test_image.PNG
error_test.thy
Email Gateway (Aug 19 2022 at 09:48):From: René Neumann <rene.neumann@in.tum.de>
Am 30.01.2013 15:47, schrieb Makarius:
On Wed, 30 Jan 2013, René Neumann wrote:
Please keep in mind, that the good ol' TTY approach with only one single
point of focus is not overall obsolete: When dealing with a single
proof, one normally only focuses on the lines one is writing.This is even before Proof General and especially before Isar proofs. Can
you show some of your proofs that you normally do?
Sorry. Probably we misunderstood each other here. By TTY(-like) approach
I meant the PG-approach of feeding line by line (resp instruction by
instruction) to the prover.
If I want to proof something (especially in apply-style which sometimes
pre-dates an isar-proof to get some inspiration of what the tools are
able to proof automatically), I really like to only feed command by
command to the prover ("what are the goals exactly after the 'with'",
"what does simp remove/unfold", "what goals does 'induction' give" ...).
Of course these points where I'm doing so might be scattered throughout
the theories. So when switching between points, the new model is clearly
better.
TL;DR: Prove one proposition ("have"): old model; overall approach: new
model.
Or did you mean a keyboard version of "hover over squiggles"?
This I meant by "would also be cumbersome".
smime.p7s
Email Gateway (Aug 19 2022 at 09:48):From: Alfio Martini <alfio.martini@acm.org>
(No email body)
Email Gateway (Aug 19 2022 at 09:48):From: Makarius <makarius@sketis.net>
On Wed, 30 Jan 2013, René Neumann wrote:
I really like to only feed command by command to the prover ("what are
the goals exactly after the 'with'", "what does simp remove/unfold",
The Isabelle/Isar proof state consists of more than just goals. For
example, you don't want to see the goal again after 'then', 'from', 'with'
etc. because they don't change it. You might want to have some editor
support to rearrange such indications of 'using' facts.
"what goals does 'induction' give" ...).
That is in fact the standard example where you can see the limitations of
the hybrid model from 2000, which is still used often today. The "induct"
proof method knows much more about the structure of the proof than just
the new subgoals than happen to pop out after it. It could propose a
canonical proof outline for the induction pattern straight away, with
placeholders for typical "by auto" proofs to finish the cases. You don't
need funny print_cases commands and its output for that, just a tiny
little more progress in Prover IDE technology.
Another example where the state output is bad are calculation proofs in
Isar. This is a very simple and basic concept, but it becomes slightly
awkward to manage with the step-by-step approach from the old times.
Makarius
Email Gateway (Aug 19 2022 at 09:49):From: Makarius <makarius@sketis.net>
On Wed, 30 Jan 2013, Alfio Martini wrote:
If I want to proof something (especially in apply-style which sometimes
pre-dates an isar-proof to get some inspiration of what the tools are
able to proof automatically), I really like to only feed command by
command to the prover ("what are the goals exactly after the 'with'",
"what does simp remove/unfold", "what goals does 'induction' give" ...).I think this point is fundamental with respect to the discussion of the
elimination of the output window in the near future.
Just to repeat canonical Isabelle terminology: "old-fashioned" -> "legacy"
-> "eliminated". The present state of the output window (for goal states)
is "old-fashioned", and there are still more situations than I would like
to see, where it is actually needed. It is unlikely to become legacy or
eliminated in general, because some tools might always need to print
things out of order.
Apply proof scripts are essential for proof exploration and also as
mentioned by René above, to the (experimental) understanding of Isabelle
automation proof procedures as well .
Back to the very start of this thread. The "more informative error
messages for Isar proof commands" from NEWS means that is now easier to
write certain structured proofs without peeking at machine states all the
time. I did that in practice, when preparing the Isabelle/Isar course at
Orleans last October. It worked approx. 90% in these examples. But the
participants then had to do it in Isabelle2012 without this convenience of
Isabelle2013.
Makarius
Email Gateway (Aug 19 2022 at 09:49):From: Makarius <makarius@sketis.net>
The Output panel gives you a full record of all messages emitted by some
command transaction, essentially as a fall-back for the traditional model,
to avoid surprises that some tools don't get their information through.
This also explains its redundancy for this "by" step that concludes a
"show":
* "Succesful attempt ..."
* Succesful proof state after it
* Unsuccessful proof state from the forked proof
Attaching more messages to the place where they belong statically, not
dynamically should clarify this further.
Mentally, it might help to understand "Output is machine state", and be
tolerant for more internal tracing happening there than in the document
model as visualized in the source.
It seems that in this situation the slight reforms of the Prover IDE were
not going far enough, but such things cannot be changed in a rash manner.
Makarius
Email Gateway (Aug 19 2022 at 09:49):From: Joachim Breitner <breitner@kit.edu>
Hi,
I haven’t tried 2013 yet, only followed the discussion, and it was not
clear to me if this is is just asking for what’s already there. But
since you mention keyboard I’d like to add that, for the sake of the
wrists of your users, please ensure that every feature is accessible
without touching the mouse. Keyboard-only control is crucial for
efficient and ergonomic use of any computer application¹.
Thanks,
Joachim
¹ with exception, maybe, of graphical stuff. But we are not yet drawing
commutative diagrams in Isabelle :-)
signature.asc
Email Gateway (Aug 19 2022 at 09:49):From: Tobias Nipkow <nipkow@in.tum.de>
Am 30/01/2013 15:39, schrieb Makarius:
On Wed, 30 Jan 2013, Lars Noschinski wrote:
I am still confused about this confusion. Taking the above specification
in isolation, it is already what happens in Isabelle2013-RC2: you see
the error "immediately" in the output of the by command, assuming that
window is open in the old-fashioned manner; it also works Proof General.
If you don't have output open, then pointing at the red squiggles of
"auto" gives the error more quickly.I think Peter's point is that he would not like to work with a version of
Isabelle where you cannot see directly what is happening at the editing focus.When you say "the editing focus" and "directly" it already has a strong bias
towards the TTY model. Isabelle/jEdit is moving more and more away from that,
as far as it becomes feasible. I am especially interested to see decent Isar
proof editing facilities, without the TTY side-conditions.
Makarius, your argument is often ideological and not ergonomic. Whenever
somebody mentions anything reminiscent of PG or TTY, it is bad per se for you
and must be abondoned. Unfortunately, some of the points, like an editing focus
and not just "legacy" but have to do something with our cognitive apparatus.
When you are working hard on a particular goal, that is your mental focus, and
you want zero distraction from it. (And you want a quick way to get back to it
when you went somewhere else.)
Here are some distracting features of Isabelle jedit: When I type a proof, the
buffer is constantly reprocessed which leads to a lot of flashing, with red
signs coming on, which makes it harder to think about the problem. When I have
mistyped a formula, it is given a pink background with grey frames around
tokens(?). This makes the formula harder to read and correct (eg the red
squiggle is harder to see). It is a bit like talking to somebody who keeps
interrupting you in the middle of a sentence whenever you pause to breathe. What
I do now is to shut that other person up with the help of one of the macros
provided here https://isabelle.in.tum.de/community/Extending_Isabelle/jEdit
until I am finished thinking and saying what I wanted to say.
Note that my argument is a cognitive one, not based on old vs new. Or, as the
Mizar guys say: Experience, not only doctrine.
Tobias
This does not mean that the Output panel of Isabelle/jEdit will just disappear
in the next release. There are applications where you do need free-form output
from commands.There are important special cases though:
(1) proof development, especially structured proof development
(2) feedback from ATPs via sledgehammer etc.
Here I can imagine more direct user interface support than the old TTY loop.
Makarius
Email Gateway (Aug 19 2022 at 09:49):From: "Tim (McKenzie) Makarios" <tjm1983@gmail.com>
This is also important for accessibility for blind users, for example.
Tim
<><
signature.asc
Email Gateway (Aug 19 2022 at 09:49):From: Makarius <makarius@sketis.net>
It was David Aspinall and myself who made these things work many years
ago, and we knew about the possibilities and technical side-conditions.
It was a big thing back then, and definitely not bad. But times are
changing, and side-conditions what can be done.
The Isabelle/jEdit document model is not so exotic, it is just
Isabelle/Isar transferred into what you see in many maintstream IDEs now,
and none of them resembles Emacs or TTY-style proof checking. E.g. see
http://www.jetbrains.com/idea/
Isar proofs are not scripts. Even in 1999 they were called documents
already, despite Proof General having a "scripting" mode only.
When I started the Prover IDE project some years ago, I made clear from
the beginning that it is not going to be a clone of Proof General, but an
exploration of what can be done beyond the accidental side-conditions of a
certain time.
I pointed out many times, that everyone who is strongly attached to Proof
General is welcome to continue its maintenance. I am even ready to give
some tips what needs to be done, but nothing has happened since
October 2011.
People who are getting uneasy about too many things changing, could get
active and do some Proof General maintenance instead.
Makarius
Email Gateway (Aug 19 2022 at 09:49):From: Makarius <makarius@sketis.net>
On Thu, 31 Jan 2013, Tim (McKenzie) Makarios wrote:
On 31/01/13 06:32, Joachim Breitner wrote:
But
since you mention keyboard I’d like to add that, for the sake of the
wrists of your users, please ensure that every feature is accessible
without touching the mouse. Keyboard-only control is crucial for
efficient and ergonomic use of any computer application¹.This is also important for accessibility for blind users, for example.
These are generic jEdit and Java GUI questions.
People who feel like doing something constructive, can start investigating
possibilities, and point out concrete solutions. There is also
sourceforge.net/projects/jedit/ to organize generic jEdit development, in
contrast to Isabelle/jEdit.
From my experience with the platform side-conditions so far, it is going
to be a lot of work to get it really right, whatever it is exactly. This
should not be misunderstood as discouragement, just as a hint that it
requires a lot of persistence to get tiny GUI aspects work in most
situations. (Everybody managed to scale his Isabelle/jEdit font-size up
and down with C-PLUS/MINUS on all platforms and national keyboards?)
Makarius
Email Gateway (Aug 19 2022 at 09:50):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Makarius,
I put in "declare[[show_types=false]] declare[[show_sorts=false]]", and
I didn't see anything extra, but I'll experiment with changing
"show_types" back and forth and see what happens.
As far as features and ways of doing things, after I get worked up, I
then remind myself that the ideas for all of this started many years
ago, and it's not the result of ideas I have about it today. I then stop
worrying/caring, and start trying to get some work done with however it
works. Speaking of "many years ago", I also keep in mind the "engine
work" that started over 40 years ago.
However, I make one last point, for the time being.
Trying to go with the new flow, I start CNTRL+hovering. However, this
brings up the final point: the human brain can process a massive amount
of information very fast sometimes.
So when I start hovering over the formula of a theorem, I get
information about, I'd say, ten times slower than what I can process the
information, and I don't think I'm exaggerating, and I don't think I'm
outside the norm.
I have a formula that's four lines long, and it has about 15 items per
line in it that can be hovered over. I start from left to right on a
line, and I drag my mouse over the items, but nothing happens other than
they turn grey, because the tooltip doesn't respond fast enough.
Well, if I'm going to drag my mouse over 45 items, then if I was writing
the software, I would give myself the ability to hover over one item and
get a massive amount of information about all of those 45 items, where
many of those items are duplicates, though seeing what is a a
duplication is not actually always quickly apparent.
I'm not writing the software, so, today, I care more about trying to use
the software as it is to get something done.
Thanks,
GB
Email Gateway (Aug 19 2022 at 10:01):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 2/1/2013 1:19 PM, Makarius wrote:
On Fri, 1 Feb 2013, Gottfried Barrow wrote:
Microsoft gets rid of the taskbar and start button in Windows 8, and
someone produces a utility to put it all back.Did you try Isabelle2013-RC2 on Windows8 already? Or anyone else?
No, I don't have Windows 8, and won't be buying a new computer any time
soon.
Regards,
GB
Incidently, my new Sony Vaio (normally used with Xubuntu) also has
Windows 8, and I actually like the way Microsoft disposed all this 3D
eye candy. KDE for example looks now quite old-fashioned compared to
that.I had to do some fine-tuning to make Isabelle work smoothly on
Windows8. So the question above is not just rethoric.Makarius
Email Gateway (Aug 19 2022 at 10:23):From: Makarius <makarius@sketis.net>
So lets take my favourite example:
term "x = x"
Here we ask the system to accept a given term formally, and produce formal
output and markup. The output is the tip of the iceberg that you see
directly, the markup is what you explore by other means, such
color schemes, formal tooltips etc.
Note that markup is both attached to the input you give and the output
that the system produces, but not in a fully symmetric manner.
So the above will give you information about the type of variable x, which
is 'a, and its sort, which is "type". You can hover over the "type" to
have the system explain to you that it is in fact class "HOL.type", and
then you jump to its definition following the implicit hyperlink.
This means you can explore that recursively by hovering over formal input
and output -- this is now mostly uniform in Isabelle2013. This unfolds a
massive tree of information, or rather a large forest, by walking a few
steps into some of its paths.
Instead, if you say:
declare [[show_types, show_sorts]]
term "x = x"
the system will interpret this as insisting in the old way: partial
annotations for some of the term positions. There is no markup, so you
can't explore the types, sorts.
Of course, there are endless possibilities to refine this further. An
obvious question is: What is a succinct "digest" (as output text) to give
you a types / sorts environment for some formal output. Old show_types /
show_sorts are traditionally very crude here. This is only a starting
point for further reworking of these ancient mechanisms. In particular, I
hope to see certain improvements done for current sledgehammer isar_proofs
output to be taken into account as well.
Makarius
Email Gateway (Aug 19 2022 at 10:28):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 2/1/2013 6:18 AM, Makarius wrote:
This means you can explore that recursively by hovering over formal
input and output -- this is now mostly uniform in Isabelle2013. This
unfolds a massive tree of information, or rather a large forest, by
walking a few steps into some of its paths.
Thanks for the explanation. And we all know how much we love hyperlinks.
This is definitely a "friendly IDE" feature you've added. It's good when
information comes to me via hyperlinks, rather than me having to go to
the information.
In case others might not have noticed yet, the hyperlinks are grey boxes
with a line around them, rather than just grey boxes.
But the way it works is that some people don't forgo the old for the
new, they keep the old and use the new also. But it may be the economics
of IDEs, that the old has to be sacrificed for the new. And that's why
there's a thriving software utility market. Microsoft gets rid of the
taskbar and start button in Windows 8, and someone produces a utility to
put it all back.
Of course, there are endless possibilities to refine this further. An
obvious question is: What is a succinct "digest" (as output text) to
give you a types / sorts environment for some formal output. Old
show_types / show_sorts are traditionally very crude here. This is
only a starting point for further reworking of these ancient
mechanisms. In particular, I hope to see certain improvements done
for current sledgehammer isar_proofs output to be taken into account
as well.
Sounds like a lot of work.
Regards,
GB
Email Gateway (Aug 19 2022 at 10:29):From: Makarius <makarius@sketis.net>
Did you try Isabelle2013-RC2 on Windows8 already? Or anyone else?
Incidently, my new Sony Vaio (normally used with Xubuntu) also has Windows
8, and I actually like the way Microsoft disposed all this 3D eye candy.
KDE for example looks now quite old-fashioned compared to that.
I had to do some fine-tuning to make Isabelle work smoothly on Windows8.
So the question above is not just rethoric.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC