Email Gateway (Aug 19 2022 at 15:22): Email Gateway (Aug 19 2022 at 15:22):From: Peter Lammich <lammich@in.tum.de>
In RC-3, I discovered the undesirable behaviour that errors are put
after the goal state in the output window.
Example:
lemma "g1" "g2" "g3"
proof -
have "False" by (simp add: list.simps)
--> The error output appears after a list of the goals "g1" "g2" and
"g3" and after a long list of simplifier warnings.
Thus, you have to scroll down to see the error output --- every time you
move the cursor in the main window from a different line to the
erroneous line. This is tedious when developing a proof, as you will go
up, change something, and then come back to the failing command multiple
times.
Moreover, the error is not visible as prominently as it used to be:
When writing "have foo by method", expecting that it works, you look at
the output window ... and it looks the same, whether your method worked
or not. Formerly, you used to see a fat red error message there, right
at the top of the output window, which is now hidden.
If using separate outputs for error, warning, tracing, and goal is not
possible, and one must have a fixed order, I would vote for the
following order:
Errors first, then the goal, then warnings, then tracing.
Of course, it would be even better to make the message types and the
order in which they appear in the output configurable!
Email Gateway (Aug 19 2022 at 15:25):From: Makarius <makarius@sketis.net>
On Mon, 11 Aug 2014, Peter Lammich wrote:
In RC-3, I discovered the undesirable behaviour that errors are put
after the goal state in the output window.Example:
lemma "g1" "g2" "g3"
proof -
have "False" by (simp add: list.simps)--> The error output appears after a list of the goals "g1" "g2" and
"g3" and after a long list of simplifier warnings.Thus, you have to scroll down to see the error output --- every time you
move the cursor in the main window from a different line to the
erroneous line. This is tedious when developing a proof, as you will go
up, change something, and then come back to the failing command multiple
times.
You don't have to scroll around, but can look directly in the main source
window -- either at the colors or the popups produced by hovering.
In PIDE the annotated source is the primary means of exposing prover
information. In the above example it works particularly well, because the
failure of the proof method invocation gets a precise error position for
the method text, not just the main command keyword as a fall-back.
If you have problems to distinguish the color overlays, you can choose
different colors in the Rendering section of Isabelle/jEdit plugin
options. Note that there is also an alpha channel for transparency.
In contrast, the Output dockable is not really part of the PIDE concepts.
It is still around as a fall-back to display proof states, and anything
else concatenated in some canonical order given implicitly by the prover.
Thus Output is merely an intermediate approximation of the real thing,
which would probably be the speculative "Preview" panel to show the
document sources with intermediate proof states, according to what is
presently relevant in the structured proof editing.
I am using myself Output relatively rarely. In the Isabelle tutorial this
Spring there was a funny incident: after approx. 2h explaining Isabelle
proof document editing, with various examples of definitions and proofs,
Timothy Bourke pointed out that I should also show the Output panel for
message display. I had just forgotten that, because it was not necessary
up to that point. But he was right that beginners often manage more
quickly to operate the Output panel than the delicate choreography with
the mouse that is required for hovering. The latter is more flexible
after some practice, though.
If using separate outputs for error, warning, tracing, and goal is not
possible, and one must have a fixed order, I would vote for the
following order: Errors first, then the goal, then warnings, then
tracing.
That reminds me a bit of old mistakes from Proof General, with certain
policies imposed by the front-end and corresponding workarounds on the
back-end. That is not fully overcome yet.
Makarius
Email Gateway (Aug 19 2022 at 15:25):From: Makarius <makarius@sketis.net>
Telling so many anecdotes, I have forgotten to point out an important
aspect in this example: the 'by' proof is forked by default, so the proof
state you see after it is the correct one after it, while the warnings /
errors belong to the independent sub-proof. The printed order is correct
according to the structure of the proof, independently of accidental
operational details in the prover.
Replacing 'by' by 'apply' or setting the option parallel_proofs to 0 does
not show a new proof state, only the cumulative messages. The verbosity
of simp-add warnings remains, but is another problem. In Isabelle2014-RC3
warnings are generally more to the point, but not yet this case.
Makarius
Email Gateway (Aug 19 2022 at 15:25):From: Peter Lammich <lammich@in.tum.de>
In think it is personal preference of how much you want to use the
mouse, and no IDE should enforce too much mouse usage.
For example, when I develop a proof, I often start throwing "apply"s at
the goal, and then want to immediately see the new subgoals, definitely
without removing my hand from the keyboard to grab the mouse.
In many cases, this "experimenting phase" leads to proving the goal, and
I then try to clean up my apply-script: Ideally, it becomes a single
"by ...".
Otherwise, I get stuck at some subgoals. Then I invoke sledgehammer
and/or try to identify auxiliary lemmas, that I then state and prove
separately using Isar.
For this mode of proof development, which is definitely not the only way
to develop a proof, but for my type of developments a very effective
one, it is essential to always see the current subgoals, also while
typing the next apply-command, without having to do some mousing or
other interaction. As there is no dedicated subgoals-panel in PIDE (as
there was in PG), I have to resort to the output panel.
As pointed out in previous mails, this is not an ideal replacement for a
subgoals-panel, but I currently try to live with its features:
Currently, the most annoying one is that the current subgoal vanishes in
favour of a "syntax error"-message while you are typing the next
apply-command.
Email Gateway (Aug 19 2022 at 15:26):From: bnord <bnord01@gmail.com>
Second that!
Best
Benedikt
Email Gateway (Aug 19 2022 at 15:26):From: bnord <bnord01@gmail.com>
Here's some experience from a course we gave last year:
We had some students that were output panel agnostic. They developed no
understanding at all about the proof state and why things didn't work as
expected. E.g. you can't simply assume ~A and show False. They had
problems with including assumptions in inductions, as for them they were
obviously part of the proof as the document explicitly stated them. The
difference in this apparent redundancy is hard to grasp from the
document without consulting the output. Also the ability to just
continue editing and getting things evaluated after many errors together
with the agnostic for the proof state lead to "nearly done proofs" that
were merely accumulations of loosely connected statements.
I don't know if these problems were always there and students ignored
the output in PG as well but I think the PIDE fosters this behaviour.
Best
Benedikt
Email Gateway (Aug 19 2022 at 15:26):From: Makarius <makarius@sketis.net>
When writing Isar proofs, there is indeed a mismatch of the proof state
vs. the proof text, stemming from the step-by-step interpretation of the
language. People who have never been instructed by one of the initial
pioneers of Isar in Munich 1998-2000 have explained to me accurately that
confusion, e.g. someone at VSL 2014 in July. This is a weakness of Isar
implemented with the side-conditions of TTY interaction -- I was aware of
that situation already 15 years ago.
Over the years I have tried to improve this bit by bit. E.g. the 'by'
command now produces proper error output on its own. The funny effect was
that long-term users who have been instructed in the workarounds from
1999-2000 don't want to change at all.
I have mentioned a speculative "Preview" panel before on this thread. If
it ever arrives, it will be just an adequate dynamic view on the emerging
proof document, based on the original source text with just the right
"state" information that is required to continue, following the structure
of the proof and its naturally unfinished state.
Makarius
Last updated: Apr 23 2024 at 16:19 UTC