# Re: [isabelle] questions about PIDE architecture

On Thu, 19 Feb 2015, Walther Neuper wrote:


But may I ask for "notes on PIDE architecture" ?


In PIDE communication between Java (i.e. Isabelle/jEdit) and Isabelle/Scala seems straight forward, because both run in the same JRE.
But how is communication between Isabelle/Scala and Isabelle/ML possible?



This question might sound trivial to some people, but I have struggled with the problem over many years, to make it really really work -- robustly, efficiently, portably.


There is a brief sketch on "PIDE Protocol Layers" in my ITP-2014 paper:

Makarius Wenzel. Asynchronous User Interaction and Tool Integration in
Isabelle/PIDE. In G. Klein and R. Gamboa, editors, Interactive Theorem
Proving (ITP 2014). 2014. Springer, LNCS 8558.

http://www4.in.tum.de/~wenzelm/papers/itp-pide.pdf

The relevant text is cited here for convenience:

\para{PIDE Protocol Layers.}  Conceptually, the two processes are
connected by two independent streams of \emph{protocol functions}.
These streams are essentially symmetric, but input from the editor
to the prover is called \emph{protocol command}, and output from the
prover to the editor is called \emph{protocol message}.
Syntactically, a protocol function consists of a name and argument
list (arbitrary strings).  Semantically, the stream of protocol
functions is applied consecutively to a private \emph{protocol
state} on each side; there are extensible tables in Isabelle/Scala
and Isabelle/ML to define the meaning for protocol functions.

The arguments of protocol functions usually consist of algebraic
datatypes (tuples and recursive variants). This well-known ML
concept is represented in Scala by case classes
\cite[\S7.2]{Scala:2004}.  The PIDE implementation starts out with
raw byte streams between the processes, then uses YXML transfer
syntax for untyped XML trees \cite[\S2.3]{Wenzel:2011:CICM}, and
finally adds structured XML/ML data representation via some
combinator library.  Further details are explained in
\cite{Wenzel:2013:CoqPIDE}, including a full implementation on a few
pages of OCaml; the Standard ML version is part of Isabelle/PIDE.
This elementary PIDE protocol stack is easily ported to other
functional languages to connect different back-ends, but actual
document-oriented interaction requires further reforms of the
prover.


See also the included fragment of some slides that explain that (and a bit more).


The citation Wenzel:2013:CoqPIDE is here: http://arxiv.org/abs/1304.6626 -- it explains more things in a prover-agnostic fashion.



Over the years watching the advent of *.scala in ~~/src/Pure/ I imagined some magic about the parallelism between the *.scala files and the *.ML files. But in

https://github.com/larsrh/libisabelle/tree/master/pide-core/src/main/scala


there are some directories from ~~/src/Pure/, and all of the copied directories contain exact copies of all the *.scala files and while dropping all *.ML files.

So, where comes communication between Isabelle/Scala and Isabelle/ML from?



As long as these are exact copies of the Isabelle/Pure Scala files, and used in a suitable environment of properties and/or process variables, they will magically work with an Isabelle/ML process that expects exactly that communication scheme.


In Isabelle/Eclipse, Andrius Velykis has made his own clone of basic PIDE functionality, although with some actual changes managed in a systematic way.


In the longer run, we need to draw further conclusions from practical experience with such derivatice projects. Somehow the idea of modularity seems to be very weak in the JVM world, and Isabelle/Java/Scala does not make this easier for mainstream project and package management tools out there. (It only makes it very easy for an Isabelle-only environment, as explained for "isabelle scalac" in the "system" manual.)


Makarius


Attachment: pide-protocol.pdf