Email Gateway (Aug 19 2022 at 17:03): Email Gateway (Aug 19 2022 at 17:03):From: Makarius <makarius@sketis.net>
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
inhttps://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
pide-protocol.pdf
Email Gateway (Aug 19 2022 at 17:03):From: Lars Hupel <hupel@in.tum.de>
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.
Those files are indeed exact copies.
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.)
I don't think modularity in the Java ecosystem is significantly weaker
than anywhere else. The problem with system integration in Isabelle is
that Isabelle has "high gravity", i.e. it usually assumes that
applications are centered around Isabelle. From that point of view, it
also makes sense that Isabelle/Scala observes ML coding conventions wrt
naming and architecture. With the rise of the document model, new
applications become possible, some of which can't (or don't want to)
adhere to that world view.
So far, I know of two major applications where significant development
effort has been spent to integrate Isabelle into existing software:
(There's also Leon+Isabelle, but that was more of a "proof of concept".)
The Isabelle integration in Clide works almost exactly in the same way
as libisabelle: They copied the Isabelle/Pure JAR into some suitable
'lib' directory. (Taking a JAR instead of the full sources has the
disadvantage that cross-compiling against different versions of Scala is
ruled out, and that the Scala version for Clide must be the same as the
Scala version for Isabelle.)
I think it is fair to say that we already have practical experience. It
might be worth getting feedback from Clide's authors (not sure if they
read this mailing list) [1].
But all this brings me back to my original point: Modularity. It would
be entirely possible to ship an "official" JAR file with some metadata
(in Java lingo: "artifact") to a repository. Integrating Isabelle into a
Scala application then becomes a matter of one line in the build definition:
libraryDependencies += "de.tum.in.isabelle" %% "pide" % "2014"
Of course, the PIDE sources would need to be enriched with functionality
to fetch an Isabelle distribution, unpack it, and build the required
components in a way that doesn't require shell scripts or Perl. (I have
that on my agenda.)
Cheers
Lars
[0] <http://clide.flatmap.net/login>
[1] their paper at ITP'14 is also quite interesting: Christoph Lüth,
Martin Ring: "Collaborative Interactive Theorem Proving with Clide"
Email Gateway (Aug 19 2022 at 17:17):From: Walther Neuper <wneuper@ist.tugraz.at>
I see, you have found a way to replace IDEs' "run configurations", and I
had the opportunity so see that used on your laptop efficiently such
that I never could follow what is going on ;-))
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?
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?
Walther
Email Gateway (Aug 19 2022 at 17:17):From: Lars Hupel <hupel@in.tum.de>
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?
I don't understand all low-level details myself, but a useful intuition
is that the JVM spawns a prover process and then exchanges XML trees
with it. This mechanism is extensible: Both processes speak a common
protocol for process management (e.g. jEdit can tell the prover "here's
an updated document", to which the prover replies "annotate this piece
of text with a warning message"), but users can extend the communication
with custom messages. These XML messages are transmitted via the
intermediate "YXML" format which is a space-efficient representation of
most of XML. A reasonable summary of this is "a custom IPC protocol".
The low-level implementation can be found in the files
'System/system_channel.scala' and 'System/system_channel.ML'. In
Isabelle2014, this is done with FIFOs or sockets (depending on the OS),
but the current development version uses sockets exclusively.
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.
Conceptually, the Scala files are not required for running the prover
process. They merely provide one way to interact with it. On the other
side, the JVM process doesn't need the ML file to do whatever it's
doing. Files of both languages could be separated without any problems
(it wouldn't even complicate the build of Isabelle).
The reason why both sources are being kept together is because there's
some symmetry which can be exploited. Some modules (e.g. XML processing,
graph algorithms) are actually the same in both languages so that it
makes sense to keep them together.
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.
I could've just taken the 'Pure.jar' file unmodified from Isabelle and
used that. There are two reasons against this:
1) I wouldn't be able to cross-compile 'libisabelle' against different
Scala versions, since 'Pure.jar' would be fixed to whatever Scala
version is currently used in Isabelle.
2) I would include some extra dependencies (e.g. Scala Swing) which are
not needed for a non-GUI library.
I did that for my work on Isabelle integration with Leon, but figured
that there ought to be a better way. Copying source files is also what
Andrius Velykis did for isabelle-eclipse.
Cheers
Lars
smime.p7s
Last updated: Apr 26 2024 at 01:06 UTC