Re: [isabelle] Isabelle's jEdit plugin: some known help documents?
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Isabelle's jEdit plugin: some known help documents?
- From: Gottfried Barrow <gottfried.barrow at gmx.com>
- Date: Tue, 31 Jul 2012 23:19:46 -0500
- In-reply-to: <alpine.LNX.email@example.com>
- References: <op.wibg4tbsule2fv@douda-yannick> <alpine.LNX.firstname.lastname@example.org>
- User-agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0
On 7/31/2012 3:17 PM, Makarius wrote:
With Isabelle/jEdit one could imagine nice videos that demonstrate the
dynamics of certain popups and other plugins, for example. I am
myself still working on the upgrade of the platform to Java 1.7 and
JavaFX 2.2, so that one might see more onboard multimedia gimmicks in
the future, with HTML5 etc.
Fame and glory on Youtube is there for the taking because there's
nothing out there to show people what an Isabelle session in jEdit can
I guarantee you, at this point, all you're lacking is marketing. If
Isabelle was a commercial operation, you would already have a flashy
promotional video out there.
For now, people don't need any instructional videos, they just need an
overview of what a proof assistant is, an overview of the associated
tools for Isabelle, some proof examples to show the interaction between
the edit buffer and the output pane, to see what they can make their
installation look like, and see what tools and plugins they're supposed
to look for when after they've installed Isabelle. It'd be like a 3 to 5
All the extra menu features that get added in the future, like
automating the use of "usedir" and IsaMakefiles, aren't going to change
the basic three panel view that's the main work space, at least not
because it's no good right now. That part of the interface and how Isar
is implemented in it is already professional quality. And it's not going
to change the different proof methods, like using intro and elim rules,
or automatic proof methods, or resorting to ATPs with Sledgehammer.
People could be shown a demo of those things in the same video.
This archive was generated by a fusion of
Pipermail (Mailman edition) and