[isabelle-dev] Remaining uses of Proof General?
makarius at sketis.net
Fri Jun 27 13:30:27 CEST 2014
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.
More information about the isabelle-dev