Re: [isabelle] questions about 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?

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
> 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.


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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