Re: [isabelle] Isabelle's jEdit plugin: some known help documents?



On Tue, 31 Jul 2012, Yannick Duchêne (Hibou57) wrote:

I feel the Isabelle community favors Emacs's ProofGeneral over jEdit (or I may be wrong), and feel there are fewer documents for Isabelle used with jEdit.

Note that Isabelle/jEdit as stable release is younger than 12 months (October 2011), but Proof General older than 12 years. Just last year at this time I was still busy chasing critical performace issues in the Scala actor communication network, which rendered the Prover IDE unusable before September 2011.


Searching the web could just return me two introductory documents, which do not covers the points mentioned above:

* Getting Started with Isabelle/jEdit
  http://www.jaist.ac.jp/~c-sterna/publications/S-IUW12.pdf

* Isabelle/jEdit — a Prover IDE within the PIDE framework
  http://www4.in.tum.de/~wenzelm/papers/isabelle-jedit-2011-1.pdf

These are indeed the two main introductory articles that I know. Users are invited to share their own experience and tricks with current Isabelle/jEdit (as of Isabelle2012). See also https://isabelle.in.tum.de/community for a still somewhat blank and boring spot for links to interesting user-contributed materials, say your own blogs, video channels etc.

Googling for Proof General (for Isabelle or Coq), one finds many funny videos for this ancient editor technology. I am particularly fond of the Proof General / Coq intro by Andrej Bauer, where he first pretends to download Proof General 4.x from the website, and then uses the specifically patched version Proof General 3.7.1.1 that is only available from the Isabelle distribution :-)

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.


	Makarius


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