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

[Makarius]

On Fri, 28 Feb 2014, Makarius wrote:

> 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 ...

Here are again some refinements towards scalable Isabelle/ML IDE support 
(presently Isabelle/075397022503):

   * ML_file references are *not* resolved by default as before, mainly due
     to performance and resource considerations.

   * A file that was opened once remains within the persistent document
     model.  This means the effect to recheck a theory hierarchy from the
     point of that file happens only once, when it is first opened.  Later
     it can be closed and re-opened without any change.

   * The main portion of semantic ML markup is now maintained persistently
     in ML, and sent to the Scala side via some Execution.print function,
     which is asynchronous, depends on perspective, and non-persistent.
     This means, whenever some already processed ML file is visited in the
     editor, substantial amounts of reports are sent over the wire on the
     spot -- there is a deep purple flash seen on the ML_file command.
     When the file becomes invisible later, these resources are freed after
     some timeout and the JVM gets a chance to perform GC eventually.

With this increasingly complex setup --- scalability is never for free --- 
I can now process Main.thy with all ML files from src/HOL/Tools/BNF/ into 
the IDE. The JVM requires less than 1.5 GB and ML about 2 GB.

It remains to be seen how this works out in practice, just keep me (and 
David Matthews) informed. We have already learned that the crash 
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2014-February/005040.html 
is somehow related to loading of big ML files under IDE control: the bulky 
report messages somehow interact badly with something else that we don't 
understand yet.

In Isabelle/38f1422ef473 I have actually changed the report channel a bit, 
to avoid huge string I/O.  This might or might not help, and the true 
reason for the crash still needs to be investigated.


 	Makarius