On Sat, 31 Aug 2013, Christian Sternagel wrote:
Assuming that the grayish background highlighting really indicates
prover activity in the background
This is outdated_color (RGB=EEE3E3 by default). It means that the
asynchronous protocol is in an intermediate state where the editor has no
confirmation from the prover about the last round of updates yet.
The prover needs to update certain internal administrative structures of
the document model until this confirmation ("the assignment") can be given
back to the editor. This requires usually a few milliseconds, but depends
on availability of CPU resources, and can get into the range of 0.5..2
seconds. (What are your hardware parameters?)
Until recently (notably in Isabelle2013) these "update -- assign" cycles
of the document model involved explicit cancellation of all running
executions of the prover *before* doing anything. There was a restart of
transactions that were still needed in the next document version. This
was OK for the majority of quick proof commands, but noticable for slow
things like 'fun' or heavy proof tools. With the integration of
sledgehammer etc. into the document model, the end of this approach was
come: accidental cancellation and restart of big ATP jobs was not
feasible.
So I reworked the whole approach quite substantially. As a consequence
the prover never stops, it merely refrains from starting new tasks. Then
edits are applied "on-line" and old tasks are cancelled afterwards if they
are no longer needed.
This means that there are fewer CPU resources available for doing the
administrative update of document content. Often it is just the protocol
thread itself, which pretends to be another worker thread for this purpose
(this guarantees progress, but a fully saturated worker farm might still
work against it).
For my part, I've seen the change in behaviour and got used to it after a
few days. It is just a matter of tradeoff between seeing more "outdated"
text views vs. long-running tools continuing all the time undisturbed. I
am not aware of a genuine problem -- if there is one you should report
that again.
I recently noticed that sometimes a "re-check" of the whole buffer
An actual "re-check" would be something else: new "execs" assigned to
existing command transactions, involving a change to pink and purple etc.
This should not happen here, unless there is something wrong in the
implementation.
In fact the new strictly monotonic model should involve fewer "re-checks".
In the past, a long-running proof step upwards in the buffer could cause a
reset to that position with a fresh start of everything in between.
when I select the second "by auto" (typically S+Home, since the courser
is positioned directly behind it after just having typed it) and then
replace the selected region by something different, the whole buffer is
highlighted (thus re-chekced or re-parsed?).
"Re-parsed" is yet another thing: whenever you do some physical edits on
the buffer, Isabelle/Scala will check on its side if anything has
structurally changed to tell the prover about it. This requires some JVM
resources, but it should not be visible in the editing process. Vacous
updates in that respect are ignored.
On the other hand, just scrolling around is a full update of the document
model, and might cause brief appearance of the "outdated" color scheme.
This is particularly relevant to the new "print functions" and "query
operations" of the document model. Uncovering parts of the text might
cause the prover to do anything from plain 'print_state' to 'sledgehammer'
(in its "auto" mode).
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
