[isabelle-dev] Inconsistent output on Isabelle/Scala message buses with parallel proofs [51069:2f50ddd3b586]
makarius at sketis.net
Mon May 13 16:39:04 CEST 2013
On Wed, 8 May 2013, Avi Knoll wrote:
> Using: changeset 51069:2f50ddd3b586
First some hints about Isabelle repository usage.
* The physical index 51069 is private to your clone. It is not relevant
to anybody else.
Even for "standard" repository clones like
http://isabelle.in.tum.de/repos/isabelle the physical changeset index is
not persistent: some months ago we had to re-clone that copy several
times, and presumably changed these addresses in the internal store.
Only the symbolic hash key counts, e.g. the abbreviated one 2f50ddd3b586
above. (The real one is 2f50ddd3b5860b830d65cb6e81c83d79c8204c98, but
that much precision is normally not required in practice.)
* To work with a repository version of Isabelle you need to have really
good reasons, and understand what it means to follow ongoing changes
quickly. For most projects it is more efficient to use the latest
official Isabelle release. Unofficial snapshots after some release tend
to become outdated more quickly than proper releases.
* Changeset 2f50ddd3b586 seems to refer to some RC version just before
Isabelle2013. So it is really outdated now. What is the point of using
that at all, instead of Isabelle2013 outright?
> I have subscribed an actor instance to the `session.all_messages`
That gives you a trace of the low-level protocol between the
Isabelle/Scala and Isabelle/ML process. That is private to the
implementation, and occasionally changes in very subtle ways.
The public API is at a higher level, using Document.Snapshot and
Session.update in certain ways you can see in Isabelle/jEdit.
An alternative is to roll your own (independent) protocol using
Isabelle_Process.protocol_command in Isabelle/ML, and wrap a suitable
Isabelle_Process receiver in Isabelle/Scala around it. That is a slightly
different story, though.
> begins processing the output after the prover has finished evaluating
> all input theories (in a related question, does anyone know how the
> output signals that it is finished processing all supplied input?).
As of Isabelle2013, there is still no official way to wrap up asynchronous
document processing, to see if it is really finished. The protocol is
motivated by interactive editor use, as you see in Isabelle/jEdit,
Isabelle/Eclipse etc. today. I can imagine a bit more here, also to have
a version of Isabelle "build" using the document model instead of
old-fashioned batch mode, but this will take more time.
> Here is an example of what might be missing (the output has been parsed
> into a local datatype, but otherwise unmodified).
I can't say from the given information if there is actually a problem
here. Empirically, Isabelle2013 works with many variations of parallel
processing of document content. Missing protocol messages for entity
markup etc. would mean that certain parts in the Isabelle/jEdit text area
remain "dead" (without hyperlinks or tooltips), but I did not see nor hear
anything like that in the past few months.
More information about the isabelle-dev