Re: [isabelle] Isabelle (JEDIT) seems slower than Isabelle(emacs)



On Wed, 26 Feb 2014, li yongjian wrote:

Isabelle/jEdit is the default Prover IDE for Isabelle Now. I have tranferred from emacs interface to jedit interface for about two months. My experience is that Isabelle/Jedit runs much slower than Isabelle/emacs interface. I guess this is caused by jedit is run on JVM.

First we should figure out if this is a genuine problem, or just the usual psychological effects of running a JVM application. What is your operating system? What are the basic hardware parameters (main memory, number of CPU cores)?

The JVM is relatively slow to start up, and needs a long warm-up to become fast. Afterwards it is actually fast, although it sometimes "looks slow". There might be also some specific Linux platform problems, e.g. due to bad graphics drivers or the use of seemingly "native" GTk, see also http://stackoverflow.com/questions/21072357/isabelle-performance-issues-with-version-isabelle2013-2


Is there some techniques to run Isabelle/Jedit much faster, e.g., diretly running Jedit in native environment (not in JVM)?

No, the use of the JVM is inherent here. In 2007/2008 I've spent a long time to investigate the general possibilities, and the JVM turned out the best option (compared to everything else). This does not mean that it is particulary elegant or pretty, but it does the job.

Note that "nativeness" has nothing to do with performance. In recent decades major programming language environments have at last moved away from the inherent problems of bare-metal program execution (as still seen in C/C++), e.g. see MS .NET "managed code".

The JVM is just a relatively early example of that, and not the best implementation of the concept. Emacs is actually of the same kind, but some generations before: it is an interpreted LISP machine, with some editing support. So Emacs is actually dead-slow: interpreted or byte-interpreted, and single-threaded.


	Makarius




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