Re: [isabelle] RC-3 puts method error after subgoals and warnings in output
On Thu, 14 Aug 2014, bnord wrote:
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.
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
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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and