[isabelle] libisabelle: Small Scala library to communicate with Isabelle



Dear list,

inspired by the obsoleted "tty" mode and a two-months old thread [1], I
decided to implement a proof-of-concept library demonstrating the
minimum amount of code needed to manage and communicate with an Isabelle
process. You can find the code at

  <https://github.com/larsrh/libisabelle>

Right now this is just a weekend project, but I'm interested to hear
your opinions and feature requests, or if you have any use case for this.

Except for a working Isabelle installation (and ISABELLE_HOME set), the
code is self-contained. You can reproduce a round-trip between Java and
ML with the following instructions:

1) Build an image of "Hello_PIDE"
   $ $ISABELLE_HOME/bin/isabelle build -d . -bv Hello_PIDE
2) Build the JAR file
   $ ./sbt full/assembly
3) Execute the example
   $ java -cp full/target/scala-2.11/libisabelle-full.jar Hello_PIDE

What the above does is starting up an Isabelle instance, sending a
command, waiting for the reply, and tearing the instance down again. The
code to achieve that is just 3 lines of Java and some more lines of ML
and can be found in the 'examples' folder.

Right now, it supports the following:
* communicating with multiple Isabelle instances at the same time
* sending simple XML-based commands
* synchronous (for Java) and asynchronous (for Scala) API

Possible extensions include:
* process lifecycle (error handling, cancellation of tasks)
* session management (invocation of 'isabelle build' ahead-of-time and
just-in-time)
* support of multiple Isabelle versions (e.g. parallel operation of
Isabelle2014 and 2015)

Cheers
Lars

[1]
<http://article.gmane.org/gmane.science.mathematics.logic.isabelle.user/10011>




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