Re: [isabelle] replace "isabelle tty"



Hello,

> (d) the functions f wrote data in XML-format, which was read from
> stdout by a Java XML parser.

firstly, I'm going to assume that your front end is running on the JVM.

I did something highly relevant in August, when I was visiting Viktor
Kuncak's group at EPFL. There, I integrated Isabelle into their existing
system which was written in Scala.

This was really easy, because the protocol with which the prover and
Isabelle/jEdit communicate is exposed as a somewhat stable API. By
putting a specific JAR file ("Pure.jar" somewhere in $ISABELLE_HOME) in
your client's classpath, you have access to all the necessary
functionality (i.e. spawning up a prover, sending protocol messages etc.).

> (a) Java started the server by
>      "isabelle tty -l Isac"
> (b) the first text line written to stdin was
>      "theory TTY_Communication imports Build_Isac begin"

This can be trivially done with the above mechanism. You can even
trigger the build of the "Isac" session first.

> (c) the client requests were ML functions   f : a1 -> .. -> an -> unit
>      written to stdin as text "ML {* f a1 .. an *}"

This is more interesting. Is the scope of what these functions do
limited, or can the user somehow specify arbitrary functions?

If the scope is limited, then you can do something like [1] and treat
the prover process as some sort of "REPL" which only understands a fixed
set of commands and acts accordingly. Notably, the support of multiple
clients in a single Isabelle session is almost trivial.

If not, there should be a way to make it work (after all, an ML block is
a regular command), but I can't offer any concrete advice there, except
maybe studying the implementation of the ML and ML_val commands in Isar.

> (1) Is the code around the removed "isabelle tty" already stable enough
> to start replacement of "isabelle tty" in our project now ?

I would say yes, even though a canonical discipline on how to write an
application using only a minimal subset of the features of PIDE has not
emerged yet.

> (2) If "yes", what are the options to replace the above (a..d) "isabelle
> tty" communication in our prototype ? Where should we start to look to
> in the Isabelle code ?

The other relevant bit in the code I wrote at EPFL is [2], although it
is cluttered with rather ad hoc session management required by the
system I was integrating with. If you're inclined, I can put together a
smaller example which should be sufficient to demonstrate the general
patterns.

There's one caveat left: All of the above presumes that using Scala is
not a problem. It's certainly possible to do all of the above with Java,
although I guess it's going to be rather verbose syntactically.

Cheers
Lars


[1]
<https://github.com/larsrh/leon/blob/8a01cfea513376821c02a2390b3a7ed3266d336c/src/main/isabelle/Isabelle_Leon/Protocol.thy#L248-L264>

[2]
<https://github.com/larsrh/leon/blob/8a01cfea513376821c02a2390b3a7ed3266d336c/src/main/scala/leon/solvers/isa/System.scala>




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