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
Description: Adobe PDF document



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.