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



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

In think it is personal preference of how much you want to use the
mouse, and no IDE should enforce too much mouse usage.

For example, when I develop a proof, I often start throwing "apply"s at
the goal, and then want to immediately see the new subgoals, definitely
without removing my hand from the keyboard to grab the mouse. 

In many cases, this "experimenting phase" leads to proving the goal, and
I then try to clean up my apply-script: Ideally, it becomes a single
"by ...".

Otherwise, I get stuck at some subgoals. Then I invoke sledgehammer
and/or try to identify auxiliary lemmas, that I then state and prove
separately using Isar.

For this mode of proof development, which is definitely not the only way
to develop a proof, but for my type of developments a very effective
one, it is essential to always see the current subgoals, also while
typing the next apply-command, without having to do some mousing or
other interaction. As there is no dedicated subgoals-panel in PIDE (as
there was in PG), I have to resort to the output panel.

As pointed out in previous mails, this is not an ideal replacement for a
subgoals-panel, but I currently try to live with its features:
Currently, the most annoying one is that the current subgoal vanishes in
favour of a "syntax error"-message while you are typing the next
apply-command.


--
  Peter





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