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
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
