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.

 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.

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.


	Makarius




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