Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle (JEDIT) seems slower than Isabelle(em...


view this post on Zulip Email Gateway (Aug 19 2022 at 13:40):

From: li yongjian <lyj238@gmail.com>
Dear Isabelle experts:
Isabelle/jEdit<https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/doc/jedit.pdf>
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.

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

regards!
yongjian Li

view this post on Zulip Email Gateway (Aug 19 2022 at 13:40):

From: li yongjian <lyj238@gmail.com>
Dear Isabelle experts:
Isabelle/jEdit<https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/doc/jedit.pdf>
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.

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

regards!
yongjian Li

view this post on Zulip Email Gateway (Aug 19 2022 at 13:41):

From: Makarius <makarius@sketis.net>
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


Last updated: Apr 20 2024 at 08:16 UTC