[isabelle-dev] Inconsistent output on Isabelle/Scala message buses with parallel proofs [51069:2f50ddd3b586]

[Makarius]

On Wed, 8 May 2013, Avi Knoll wrote:

> Using: changeset 51069:2f50ddd3b586
> http://isabelle.in.tum.de/repos/isabelle/rev/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` 
> Event_Bus.

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.


 	Makarius