Re: [isabelle] The Isabelle Server: responsive control of prover sessions



On 29/03/18 11:58, Walther Neuper wrote:
>>
> Our application
>     https://intra.ist.tugraz.at/hg/isa
>     https://intra.ist.tugraz.at/hg/isac
> (server and client respectively) uses libisabelle
>     https://github.com/larsrh/libisabelle
> to connect Isabelle with our Java/Scala front-end. This connection is
> reliable and well maintained over Isabelle versions.
> 
> If I understand correctly from a quick review of the material pointed at
> above, then the new Isabelle server would allow to replace libisabelle
> with little effort and open new prospects for further development of our
> application.

I can't say much about libisabelle: I've read the sources 2-3 times,
without really understanding how it works and what it does. My general
impression is that it connects to a raw toplevel environment without
PIDE document context.

The point of the new Isabelle Server (which was already planned in
2009/2010 but only now implemented) is to have a "headless" PIDE
connection. I.e. some other program throws theory sources declaratively
at the server and gets feedback according to the built-in policies (e.g.
for parallel checking).


> So we would be interested to invest the efforts required. However, we
> would probably need some help, since we have no expert in our team to
> deal with intricacies of TCP/IP etc presently.

You do not have to understand TCP/IP. Connecting to a server e.g. on the
JVM is trivial, you merely open the socket like this (with the port
reported by the "isabelle server" tool):

  $ isabelle scala

  import java.net.{Socket, InetAddress}
  val socket = new Socket(InetAddress.getByName("127.0.0.1"), port)

Now you can read/write over the socket byte channels as usual. Here is
the most primitive example (with the password reported by the "isabelle
server" tool):

  import isabelle._
  socket.getOutputStream.write(UTF8.bytes(password + "\n"))
  socket.getOutputStream.flush()

  socket.getInputStream.read()
  socket.getInputStream.read()
  socket.getInputStream.read()

The latter should give "OK ", i.e. 79, 75, 32 (the response is actually
a bit longer).


The remaining work is to read and write messages in the format described
in chapter 4 of the "system" manual. It also involves JSON syntax.


If you are already on the JVM platform, you can bypass the server and
use the library functions for Scala (not Java) directly. E.g. like this:

  $ isabelle scala

  val options = Options.init()
  val session = Thy_Resources.start_session(options, "HOL", progress =
new Console_Progress)
  val result = session.use_theories(List("~~/src/HOL/ex/Seq"), progress
= new Console_Progress)

Then you can inspect result.nodes, result.messages(node_name) etc. -- it
provides a representation that is closer to PIDE, while the server
imitates command-line output, see also
http://isabelle.in.tum.de/repos/isabelle/annotate/ad735a551a11/src/Pure/Tools/server_commands.scala#l200


	Makarius




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