[isabelle-dev] NEWS: improved support for Isabelle/ML
makarius at sketis.net
Fri Feb 28 14:14:04 CET 2014
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.
More information about the isabelle-dev