Re: [isabelle] RC-3 puts method error after subgoals and warnings in output
On Wed, 13 Aug 2014, Makarius wrote:
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.
lemma "g1" "g2" "g3"
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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and