Email Gateway (Aug 22 2022 at 09:53): Email Gateway (Aug 22 2022 at 09:53):From: Peter Lammich <lammich@in.tum.de>
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.
Email Gateway (Aug 22 2022 at 09:53):From: Makarius <makarius@sketis.net>
The main place to retrieve errors and warnings is the text area, via the
squiggles or icons in the gutter.
The main place to look at goal states is the Output buffer -- state and
tracing information are somehow "internal" and not shown directly in the
text.
The scheme we now see in Isabelle2015 is a consequence of continuous
reforms of the message model. It is there for several months already, and
we've had several weeks of RC testing.
Unless there is a fundamental flaw still hidden somewhere, it is not going
to change again for this release line, just a few days before final
lift-off.
Makarius
Email Gateway (Aug 22 2022 at 09:54):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
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.
We’re seeing a similar thing with the sledgehammer panel: the asynchrony works well, but depending on what the user is doing when they are proving, they will want to see the output before they do anything else. That doesn’t mean that not many other useful things can’t go on in the rest of the document, but the user will be synchronously waiting for the sledgehammer output before proceeding.
Basically, the asynchrony of Isabelle and the document model have surpassed that of the user’s brains, so that side has now become the bottleneck.
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 09:55):From: "C. Diekmann" <diekmann@in.tum.de>
Now that you mention it, I also prefer errors before normal output.
Probably it's too late now but I hope we can get this behavior back
soon.
Email Gateway (Aug 22 2022 at 09:55):From: Makarius <makarius@sketis.net>
The reason why this changed in Isabelle2015 is that "state" output is not
normal output.
Having things "back" is no progress. One always needs to look at the
whole picture, as it is emerging step by step over many years.
Makarius
Email Gateway (Aug 22 2022 at 09:55):From: Peter Lammich <lammich@in.tum.de>
One only have to be careful not to "progress away" from your users,
or forgetting to introduce well-tested and practical working alternative
to a feature that gets abandoned for the sake of progress ...
Using the output window which displays the proof state and errors is the
de-facto method how proofs are developed today by most users. If you
abandon the possibility to develop proofs this way because it is
old-style, better be sure that the new-style alternative is viable and
works for your users.
I have worked for two days with RC5 now, and found it the most annoying
difference compared to Isabelle-2014, that I cannot easily see the error
output of proof commands when trying to find a proof ... Instead of the
error, it shows me the subgoals on which I attempted the proof method,
and I have to scroll down, or hover the mouse over the squiggly lines
and wait to see the error, which is the thing I am mostly interested in
in that moment ... people that do not regularly work with big subgoals
perhaps find it not that annoying, because they still see the error
message in the output window. However, I doubt that many people
regularly look at errors by hovering the mouse over the sqiggly
lines ...
Email Gateway (Aug 22 2022 at 09:55):From: Makarius <makarius@sketis.net>
More than 5 weeks ago at RC1 this could have been reconsidered for this
release, but not at RC5 in the last moment before the lift-off.
Makarius
Email Gateway (Aug 22 2022 at 10:15):From: Tobias Nipkow <nipkow@in.tum.de>
We are now past the release but this unpleasant behaviour is still with us.
Please do not fortget about it.
Thanks
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 10:15):From: Makarius <makarius@sketis.net>
The next release will probably happen next year, so there is plenty of
time to figure out if there is anything to be done here at all. So far
this thread merely proved a lack of serious testing of release candidates.
As usual, I need a proper description of what is perceived as
"unpleasant", "broken", "bug" etc. The initial message on this thread was
about message order wrt. different kinds (state vs. non-state, especially
warning, errors etc.). This is e.g. illustrated in the following example:
lemma A
apply (tactic ‹fn st => (warning "foo"; all_tac st)›)
Here the ordering is the same in Isabelle2014 and Isabelle2015.
There were other changes in Isabelle2015, to address earlier complaints
from users. Maybe that had an adverse effect elsewhere. Or maybe it is
just a matter to get used to certain new behaviour.
Makarius
Email Gateway (Aug 22 2022 at 10:16):From: Tobias Nipkow <nipkow@in.tum.de>
On 20/06/2015 23:36, Makarius wrote:
On Sat, 20 Jun 2015, Tobias Nipkow wrote:
>On 25/05/2015 11:56, Makarius wrote:
On Mon, 25 May 2015, Peter Lammich wrote:
I have worked for two days with RC5 now, and found it the most annoying
difference compared to Isabelle-2014More than 5 weeks ago at RC1 this could have been reconsidered for this
release,
but not at RC5 in the last moment before the lift-off.Makarius
We are now past the release but this unpleasant behaviour is still with us.
Please do not fortget about it.The next release will probably happen next year, so there is plenty of time to
figure out if there is anything to be done here at all. So far this thread
merely proved a lack of serious testing of release candidates.
The thread proves that there are at least three users who do not like the new
behaviour and that you prefer to blame others.
As usual, I need a proper description of what is perceived as "unpleasant",
"broken", "bug" etc. The initial message on this thread was about message order
wrt. different kinds (state vs. non-state, especially warning, errors etc.).
Peter's first email was clear on this, and your replies showed that you
understood what he meant. To jog your memory, try this:
lemma A
apply(rule refl)
This is e.g. illustrated in the following example:
lemma A
apply (tactic ‹fn st => (warning "foo"; all_tac st)›)
No, it is not. You are suddenly dragging in warnings, but this thread is not
about them.
Tobias
Here the ordering is the same in Isabelle2014 and Isabelle2015.
There were other changes in Isabelle2015, to address earlier complaints from
users. Maybe that had an adverse effect elsewhere. Or maybe it is just a
matter to get used to certain new behaviour.Makarius
smime.p7s
Last updated: Nov 21 2024 at 12:39 UTC