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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
