Email Gateway (Aug 18 2022 at 16:12): Email Gateway (Aug 18 2022 at 16:12):From: Holger Gast <gast@informatik.uni-tuebingen.de>
Dear Joachim,
The issue arises from I3P trying to have the messages of previous
commands available for the user for inspection. For this to work,
Isabelle has to print the goal state, which may take some time
(sometimes > 100ms, or even more for really large goal states).
I had already noticed this, but it was never severe enough to prompt action.
Since we agreed that the availability of previous messages is desirable,
simply turning off the output is no solution.
I have therefore added to the I3P framework the notion of
"lazy messages", of which Isabelle only sends a "proxy" with an identifier,
and internally keeps the information for generating the message
on request. (Due to the structure-sharing, purely functional
representation employed throughout Isabelle, this is not a
major overhead.) When the user points the UI to a lazy message,
it is requested from Isabelle on the fly.
With this setup, the perceived processing speed in
release 1.0.8 has increased very much.
Lazy messages, as implemented, also cover more general scenarios
than just the goal output. For instance, I have had good results
for bulk trace messages where the proxy contained enough information
to let the user decided whether the message is relevant at all.
If this is interesting to other people, I can provide more details.
Also, the LazyMessageHandler in the Isabelle2009Driver
(in the 1.0.8 source code) explains the essential idea of how to
garbage-collect message references across the process boundary
using Java's WeakReference/ReferenceQueue mechanisms.
Thank you very much for pointing this out, and also for the offline
discussion and for testing the changes beforehand. It certainly
raised very interesting design & programming challenges :)
Holger
Last updated: Apr 27 2024 at 01:05 UTC