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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
