Re: [isabelle] questions about PIDE architecture



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

* Isabelle/Eclipse with Eclipse being the "center of the universe"
* Clide [0] with a Play! web application

(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"




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