Re: [isabelle] RC-3 puts method error after subgoals and warnings in output




Am 13.08.14 19:59, schrieb Makarius:
In PIDE the annotated source is the primary means of exposing prover information.

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




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