[isabelle-dev] Remaining uses of Proof General?

[Makarius]

On Fri, 27 Jun 2014, Peter Lammich wrote:

> SCALABILITY & STABILITY:
>
> * Isabelle/jEdit gets really slow and unresponsive when many files are
> loaded (you have to wait seconds for a keystroke to show its effect). As
> all prerequisite theories (not in an image) are automatically loaded,
> this is unavoidable. In PG, it's no problem to load a theory with many
> prerequisites, nor to have many buffers open simultaneously.
>
> NOTE: This problem could be solved in my case by 1) giving jEdit a
> ridiculously large amount of heap space (4Gb) and, 2) using images for
> prerequisite theories.

There is a conceptual difference here: PG edits only a single file, but 
the Prover IDE a whole project.  This usually works, if the resources that 
are available on current hardware is actually used.

A JVM heap space of 4 GB is not ridiculously large, but perfectly normal 
-- a cheap high-end laptop as at least 8 GB.  On my 5 years old 
workstation, I use 4-8 GB JVM heap routinely.  The l4.verified project 
has reported 16 GB of JVM heap requirements, which I would call quite 
reasonable for such a large thing.


If there are remaining resource problems, they need to be backed-up by 
proper experimental data: hardware parameters, Poly/ML memory options, JVM 
memory options, concrete examples etc.

It does not make sense to use Isabelle/jEdit in a way that PG was used 10 
years ago, concerning these important side-conditions.


 	Makarius