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

[Dmitriy Traytel]

Am 31.03.2014 23:14, schrieb 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.

This is great, especially since BNF is now distributed all over 
HOL---some parts (Ctr_Sugar.thy) are loaded very early, some in the 
middle (up to BNF_LFP.thy), and some towards the end, even after 
List.thy (BNF_GFP.thy). Now I can lookup library functions loaded in 
Ctr_Sugar, when working on the ML files in BNF_GFP without waiting for 
everything in between to reload.

Do I understand the third bullet point correctly, in that closing ML 
buffers is not required anymore (to save space), since the memory 
associated to unfocused buffers will be freed by GC eventually?

Thanks for the hard work towards the best IDE for a functional 
programming language!
Dmitriy