Re: [isabelle] replace "isabelle tty"



Hello,

> So far I understood, that
> (1) Session.protocol_handler starts a persistent session

it works in the opposite direction. The JVM process spins up a prover
process. Then, the protocol is initialized and both sides "register"
some handler for bidirectional communication. That is,
"Session.protocol_handler" tells the JVM that the specified class should
receive messages from the prover.

> (2) Isabelle_Process.protocol_command takes a string list, interpretes
> the strings, accordingly executes a predefined collection of ML
> functions and returns results as strings.

"protocol_command" is in some sense "dual" to "protocol_handler": it
tells the prover that the specified function should receive messages
from the JVM. You're correct in that the function is called with some
strings and can then do whatever is necessary. However, it does not
actually return anything.

Bi-directional communication in the PIDE model is message-driven. That
means that sending data has a "fire and forget" semantics: It
immediately returns and there's no waiting for a reply or anything. Both
JVM and prover can send messages to each other at any point in time.

In the sources, you can see that the "exec" function actually always
sends a reply, but does so via "protocol_message", which generates a new
message which is completely independent from the one the handler
received earlier.

> However, I could not yet find out, how to use isabelle_process or the
> isabelle wrapper (or what else?) to feed the strings such that they
> drive (1) and (2).

As written above, your JVM application drives the whole process. You
invoke the appropriate functions for starting up the prover, load the
"Isac" section where your handler is waiting for input. Then you can
send messages to your handler.

I hope that sheds some light onto the somewhat delicate procedure. We
could definitely do with more documentation on the system integration
aspect of Isabelle/Scala (which would presumably go into system.pdf,
whose chapter on that topic is very sparse). I reckon that with the
removal of "isabelle tty", more applications of Isabelle/Scala will emerge.

Cheers
Lars




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