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 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.

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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.