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



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




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