Email Gateway (Aug 22 2022 at 10:17): Email Gateway (Aug 22 2022 at 10:17):From: Makarius <makarius@sketis.net>
(This is a relaunch of a thread that ended up containing mostly rubbish.
Here is another attempt to shed some light on the factual situation.)
The latter aspect has actually changed here:
changeset: 59331:4139db32821e
user: wenzelm
date: Fri Jan 09 20:39:17 2015 +0100
files: src/Pure/PIDE/command.ML
description:
non-strict print_state: display old proof state on failure, e.g.
unfinished command;
That is from 09-Jan-2015, and it is the new behaviour in Isabelle2015 on
this thread that was not articulated so far. Try this example in
Isabelle2014 vs. Isabelle2015 to see the difference:
lemma A
apply fail
Of course, a method application error is also an error, so the old state
is printed first and the error message second. Thus the error might get
obscured by long proof states, which was the original starting point
above.
The deeper problem is cluttering of Output with too many different things,
and the lack of a dedicated panel just for proof state output. I was
actually thinking about reformed proof state output 1-2 weeks ago, but got
distracted again by the noise here on the mailing list.
Makarius
Email Gateway (Aug 22 2022 at 10:17):From: Peter Lammich <lammich@in.tum.de>
On Di, 2015-06-23 at 10:19 +0200, Makarius wrote:
(This is a relaunch of a thread that ended up containing mostly rubbish.
Here is another attempt to shed some light on the factual situation.)On Thu, 21 May 2015, Peter Lammich wrote:
The output window shows the normal output (e.g. the current subgoals)
before the error output, (e.g. tactic failed).This is very inconvenient if the list of goals is longer, and you have
to scroll down every time to see the error message.In Isabelle2014, it was fine, and it showed
errors, then normal output, then warnings.btw: I reported the same issue for some Isabelle2014-RCx, it got fixed
for 2014, and now we have it back again.Can you explain precisely what you reported for Isabelle2014-RCx? What
was the "issue" and what was the "fix".
As you pointed out, it was already discussed in
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-August/msg00115.html
in the release, the error messages then appeared before the subgoals,
or, more precisely, the subgoals did not appear explicitly at all, but
the error message contained a list of subgoals.
In Isabelle2015, the last goal state before the failing command seems to
get printed, too --- before the error message. This behaviour has a
positive and a negative effect on (my personal) workflow, which somewhat
coincides with your analysis:
Positive: When typing commands, in particular those involving inner
syntax like <have "very-long-term">, I can see the current goal-state
all the time. In Isabelle2014 you saw "syntax error" or "type error"
most of the time, and had to go back with the cursor to see the
goal-state. I appreciate this behaviour, because, during typing such a
command, you are mostly interested in the previous goal state ... not in
the bogus information that you have a syntax error b/c typing is not
completed yet.
Negative: As already reported before, if you have finished typing the
command, you are expecting that it works. If it does not, you are mostly
interested in the error message, and the proof state of the previous
command is of less importance.
As you point out, this behaviour was introduced in 2015. Note that the
overall problem was introduced with the processing model of PIDE, and
did not exist in Proof-General: There, by issuing a "goto this position"
The deeper problem is cluttering of Output with too many different things,
and the lack of a dedicated panel just for proof state output.
For those people with large screens, this may be a good solution. It
already worked nicely for PG, where I usually used the "3-pane" mode, or
had three windows: Text, Goal-state, Errors/Warnings.
To make up for a nice layout, I would like to dock one panel to
right-top, and the other to right-bottom. Does jedit support such
docking positions, that go beyond left,right,top,bottom?
If you work on a small screen (laptop), you probably still want to have
a mode that consumes less space, and sensibly mixes the outputs.
However, I do not know how a PIDE-like asynchronous IDE can guess what
the user currently wants to see. Perhaps, you could try a heuristics on
the type of error, something like:
Syntax-errors are displayed after the goal-state, failed method errors
before the goal-state.
Peter
Email Gateway (Aug 22 2022 at 10:17):From: Peter Lammich <lammich@in.tum.de>
One solution that does not involve too much implementation effort might
be to not include the goal-state into the error message, and output this
shorter error message before the goal-state.
While the user is typing, he would see a short error message that he
could ignore, followed by the goal state.
When the user is inspecting the (error-)result of the command, he would
see the error message first. Warnings should still be printed after the
goal-state
Email Gateway (Aug 22 2022 at 10:18):From: Larry Paulson <lp15@cam.ac.uk>
Yes — this might be OK.
Larry
Email Gateway (Aug 22 2022 at 10:18):From: Dmitriy Traytel <traytel@in.tum.de>
But this would also mean that one does not see the intermediate goal
state if something goes wrong in the terminal method slot of by.
lemma "P (xs :: 'a list)"
by (induct xs) auto
This is more useful when repairing existing proofs, rather than writing
new proofs, though.
Dmitriy
Email Gateway (Aug 22 2022 at 10:18):From: Makarius <makarius@sketis.net>
On Tue, 23 Jun 2015, Peter Lammich wrote:
The deeper problem is cluttering of Output with too many different
things, and the lack of a dedicated panel just for proof state output.
For those people with large screens, this may be a good solution. It
already worked nicely for PG, where I usually used the "3-pane" mode, or
had three windows: Text, Goal-state, Errors/Warnings.To make up for a nice layout, I would like to dock one panel to
right-top, and the other to right-bottom. Does jedit support such
docking positions, that go beyond left,right,top,bottom?
We've had this topic occasionally on the mailing list. The default
dockable window manager of jEdit can't do that, but it is a general
"framework", so plugins can implement their own policies. Anybody
interested in some Java/AWT/Swing window management should subscribe to
the jedit-devel mailing list and start a discussion there.
So far I've done myself only very minimalistic tuning of the built-in
window manager, e.g. to add the "Detach" menu item.
If you work on a small screen (laptop), you probably still want to have
a mode that consumes less space, and sensibly mixes the outputs.
However, I do not know how a PIDE-like asynchronous IDE can guess what
the user currently wants to see. Perhaps, you could try a heuristics on
the type of error, something like: Syntax-errors are displayed after the
goal-state, failed method errors before the goal-state.
In ancient times when Proof General was alive and young (10-15 years ago),
people had rather large displays and power-users even a second display
just for goal state output.
Today people expect to be able to do big things with tiny mobile devices.
With a really high resolution display (4K, 5K, Retina) it might actually
work, if the font size is set to traditional 12px.
Makarius
Email Gateway (Aug 22 2022 at 10:18):From: Makarius <makarius@sketis.net>
The observation by Dmitriy is correct.
The current printing of goal state errors is the result of various reforms
in the past few years. That relatively new behaviour is actually the
reason why I usually do many things without ever looking at the Output
window, often having it closed over a long stretch of time: the message
under the red squiggles usually provides the relevant bits to see what is
missing to finish a proof step.
As already explained on earlier instances of the thread, any built-in
policies to reorder messages in output don't work. We've had that in
Proof General, and it converged to a big mess over the decades. In 2007
that actually caused total existence failure between Proof General 3.x and
4.x. Then I introduced "isabelle tty" as temporary workaround; then
"isabelle jedit" a bit later.
On a multi-window GUI there is no point to squeeze everything into a
single linear output. The Query panel already provides a different way to
view a proof state, independently on Output. Such things are relatively
easy to make, and don't require artificial intelligence from the system to
guess what the user wants to see.
Makarius
Email Gateway (Aug 22 2022 at 10:18):From: Peter Lammich <lammich@in.tum.de>
So we could extract two feature requests:
1. Allow for a separate errors/warnings and a proof state panel.
Ensure that they can be laid out nicely, such that the user can view
them both simultaneously. In current jedit, the panels could be detached
and the layout been done by the OSs' window manager.
2. Change the current output/proof state panel to display (short
versions of) error messages before warnings. The errors displayed on the
squiggly lines may of course still contain the proof state. I know that
this may be a technical problem, b/c (as far as I know) error messages
are generated by the ML-side, and not touched by the IDE.
Email Gateway (Aug 22 2022 at 10:18):From: Tobias Nipkow <nipkow@in.tum.de>
I recommend to reread Gerwin's comment on red squiggles in the earlier thread:
I’m not as worried about the scrolling as Peter (you could set goals_limit for
instance, although I’d prefer not to have to), but I do have to point out that
the squiggles can’t be the main interaction mechanism for errors. They are
popups: you have to pick up the mouse, navigate there, and wait to see them. If
the statement is big, the message sometimes obscures what you typed. That's too
disruptive as main mechanism.
It’s good to have the squiggles for errors (esp for position indication), and
they work very well for warnings, but when you’re writing your proof, your brain
doesn’t work as asynchronously as the document model. You will still have your
mental focus at one point and you will still want to see the result of your last
action as quickly as possible and react if it is an error. When you’re writing
the proof, your mental focus is on the output window, so that’s where errors
reports will cause the least mental overhead.
I couldn't agree more.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 10:18):From: Makarius <makarius@sketis.net>
I read that, and it is one of the few things that are not rubbish on the
other thread.
Gerwin merely described observations, without pretending to know how
things work or how they should be done.
Makarius
Email Gateway (Aug 22 2022 at 10:18):From: Makarius <makarius@sketis.net>
On Tue, 23 Jun 2015, Peter Lammich wrote:
- Allow for a separate errors/warnings and a proof state panel.
Ensure that they can be laid out nicely, such that the user can view
them both simultaneously. In current jedit, the panels could be detached
and the layout been done by the OSs' window manager.
That is relatively simple, as I have pointed out already.
I can immediately imagine further improvements, but it will require to
move further and faster beyond old customs, and that has often been
inhibited in the past few years.
- Change the current output/proof state panel to display (short
versions of) error messages before warnings. The errors displayed on the
squiggly lines may of course still contain the proof state. I know that
this may be a technical problem, b/c (as far as I know) error messages
are generated by the ML-side, and not touched by the IDE.
That is the "AI" approach to messages again. It has already been
disproven many times in the past.
Errors and warnings need to be produced and managed as uniformly as
possible. Special treatment and variations tend to cause unexpected
breakdown. We've had that e.g. in the goal state output in tactic failure
when it was first introduced, and only shortly after the release back then
you discovered that the goal was printed without the flags of normal goal
state printing, causing denial-of-service in the front-end for big states.
Makarius
Email Gateway (Aug 22 2022 at 10:18):From: Harry Butterworth <heb1001@gmail.com>
In Isabelle/jEdit, I've also noticed needing to scroll to see error
messages and goals disappearing when I start typing. I have been using
multiple views to get everything I want on the screen at once and using
copy paste to keep a snapshot of a goal that I want to look at.
Remainder of this email wanders off topic...
In ancient times when Proof General was alive and young (10-15 years
ago), people had rather large displays and power-users even a second
display just for goal state output.Today people expect to be able to do big things with tiny mobile devices.
With a really high resolution display (4K, 5K, Retina) it might actually
work, if the font size is set to traditional 12px.
I have run eclipse on my phone and it does work for a "Hello world!" demo
but isn't usable because the interface isn't optimised for touch and using
a mouse and keyboard puts you too far away from the tiny screen. I think
Isabelle/jEdit would have the same problem on a small high res display.
At work and home, I switched to using 4K TVs for Isabelle/jEdit. I have
one flat one and one curved one. The better of the two is the curved one -
a 48" 4K SAMSUNG 48JU6800 (driven by a 9 series NVIDIA GTX @ 60Hz in UHD
colour mode to get 4:4:4 chroma for pixel perfect text). The curve is
definitely a good thing as the left and right edges seem much farther away
on the flat one even though it is smaller at 40".
Both 4K TVs are very usable at normal monitor sitting distance and about
the same pixel density as traditional monitors so text isn't tiny.
My next step after getting the big screen was to replace my core i7 920
with a (used) Xeon x5680 and overclock it to 4.7 GHz using a new Corsair
H100i cooler and my existing ASUS Rampage II Gene motherboard and Seasonic
M12D PSU.
I used run_tests from seL4 to check stability and benchmark performance and
found that overclocking the RAM also made a significant improvement.
I thought I'd share the details because the big screen and massive
overclock made a huge improvement to usability of Isabelle/jEdit which now
feels fairly snappy.
Also it's a data point indicating available screen real estate for extra
windows for goals and error messages.
Email Gateway (Aug 22 2022 at 10:19):From: Makarius <makarius@sketis.net>
I wouldn't call this off topic. It is always interesting to hear about
working user scenarios.
The above sounds like a fairly good machine for the high-end gaming that
interactive theorem proving is today :-)
On my modest 24" Dell 4K monitor (P2415Q) I actually encountered GUI
scaling problems. Some of my findings are explained in the Isabelle/jEdit
manual section 2.1.2 "Displays with very high resolution", but that is
only a start on that topic. If there is further experience with
high-resolution GUIs, it is worth a different thread on the mailing list.
The next jEdit release will cope with that better, but it is not yet
available.
Makarius
Email Gateway (Aug 22 2022 at 10:20):From: Tobias Nipkow <nipkow@in.tum.de>
On 23/06/2015 18:52, Makarius wrote:
On Tue, 23 Jun 2015, Tobias Nipkow wrote:
I recommend to reread Gerwin's comment on red squiggles in the earlier thread:
I’m not as worried about the scrolling as Peter (you could set goals_limit for
instance, although I’d prefer not to have to), but I do have to point out that
the squiggles can’t be the main interaction mechanism for errors. They are
popups: you have to pick up the mouse, navigate there, and wait to see them.
If the statement is big, the message sometimes obscures what you typed. That's
too disruptive as main mechanism.It’s good to have the squiggles for errors (esp for position indication), and
they work very well for warnings, but when you’re writing your proof, your
brain doesn’t work as asynchronously as the document model. You will still
have your mental focus at one point and you will still want to see the result
of your last action as quickly as possible and react if it is an error. When
you’re writing the proof, your mental focus is on the output window, so that’s
where errors reports will cause the least mental overhead.I read that, and it is one of the few things that are not rubbish on the other
thread.
Speak for yourself, but don't insult other contributors to this list. We don't
call red squiggols rubbish either.
Tobias
Gerwin merely described observations, without pretending to know how things work
or how they should be done.Makarius
smime.p7s
Last updated: Apr 26 2024 at 16:20 UTC