I've made another round of refinements (presently at
Isabelle/f7ceebe2f1b5). There were some situations where the change
propagation of blobs (auxiliary files) versus theories was not right,
leading to an invalid perspective of the latter, and causing it to be
rechecked to the bottom whenever it lost its physical editor view. This
and some other fine points are now sorted out.
Note that the basic model is this: auxiliary files are either managed by
the editor (via document updates) or the prover (via file-system access).
If that status changes, e.g. by opening or closing some ML file in the
editor, the corresponding thy_load command (e.g. 'ML_file') is updated,
and the theories rechecked from that point (according to their own
perspective, not the whole text as before). Anything apart from that is
probably a mistake.
I could try harder to manage files always from the editor side, as done
for theories, but then we hit the performance problems reported below ...
On Tue, 18 Feb 2014, Dmitriy Traytel wrote:
However, once I had to restart Isabelle as JEdit became quite
irresponsive (using almost 4GB of memory, forced GC didn't help). Maybe
I just hat too many ML files open (I usually don't close them once
opened) or my ML files are just too big: e.g.
~~/src/HOL/Tools/BNF/bnf_gfp.ML, although on a fresh start after opening
just this ML file the system is responsive (with some understandable
delay in displaying the markup, but instantly processing edits). Maybe
slightly lighter type annotations (at every constant/variable rather
than at every subterm) would dodge such problems?
I have experimented with this a bit, opening
$ISABELLE_HOME/src/HOL/Complex_Main.thy and *all* ML files (using
"isabelle build -nl HOL" to figure that out). This basically works, but
the poly and java processes both converge towards 2-4 GB. Note that I
have reduced the overall size of PIDE markup trees in
Isabelle/33ad12ef79ff (independently of the above observation), so it
might help a little.
Main HOL has become quite huge, and a lower middle class machine with only
8 GB is barely sufficient to edit it with everything continuously checked,
including all ML modules (which now outweigh the theories).
For the moment I recommend to "swap out" ML files manually, by closing the
jEdit buffer. Then the prover takes over for that piece of source, and no
PIDE markup is produced. In the experiment with all ML files, this makes
a difference of 2600 MB vs. 600 MB JVM heap size.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
