[isabelle-dev] Feedback from a Isabelle tutorial

[Christian Sternagel]

On 06/24/2011 01:37 PM, Makarius wrote:
> On Fri, 24 Jun 2011, Lukas Bulwahn wrote:
>
>> Johannes Hoelzl and me, gave a two-and-half-hour tutorial to Isabelle
>> at a workshop meeting of PhD students in computer science in Dagstuhl
>> (cf. http://www.model.in.tum.de/um/vernetzungstreffen/).
>
> Thanks for the feedback. I would like to add the page of a recent course
> of ours at Paris: http://www.lri.fr/~wenzel/Isabelle2011-Paris/ where we
> were using the Isabelle/jEdit IDE of official Isabelle2011. The feedback
> was quite positive even with this old version.
>
> My general impression is that the "first contact" with Isabelle has
> become much easier. Things are still lacking for power users, but there
> has been quite some progress in the past few months. I have already
> reworked the rendering in the editor substantially, and are now about to
> revise the interaction model again to burn less CPU cycles.
This reminds me that I also wanted to give feedback concerning 
Isabelle/jEdit. In a recent course (using Isabelle2011)

   http://cl-informatik.uibk.ac.at/teaching/ss11/eve/

I initially introduced students to GNU Emacs + Proof General as well as 
jEdit (as possible Isabelle interfaces) and then let them freely choose 
their preferred interface. Almost all students (except those that where 
using Emacs already heavily before) exclusively used jEdit after a while.

It is a known issue (if an issue at all) that in Isabelle/jEdit it is 
sometimes necessary to cut-and-paste some lines in order to 
"synchronize." Some students found this unexpected or even weren't able 
to solve exercises in the beginning since they didn't know that the 
solution was cutting and pasting. After I told them, everything went fine.

Overall also in this course the feedback was quite positive.

chris
>
>
>> Overall, we got a positive feedback from many participants. Working
>> with the interaction model of Isabelle/jEdit seemed not to pose any
>> problem for the students and we had no crash or unexpected behaviour
>> with the current version.
>
> Good to hear. If you do encounter unexpected behaviour, just tell me so
> that I can address it.
>
>
> Makarius
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>