[isabelle-dev] NEWS: improved support for Isabelle/ML

[Makarius]

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