Re: [isabelle] replace "isabelle tty"



Lars,

thank you for the helpful explanations.

Now I studied [2] and see, that this scala colde establishes the other side for communication with Session.protocol_handler and Isabelle_Process.protocol_command from [1]. So I prepare to adapt both [1]+[2] for Isac and come back to your discussion with Makarius:

> My impression in
> the past 7 years was that these things do change between major releases
> of Scala, and direct Java access is not properly supported.

Indeed. The only guarantee is calling Java from Scala, and even that
breaks from time to time because of mismatches between their type systems.
;-(( we need to call Scala from Java
> The Isabelle/Scala attitude towards that problem is to ask users to
> write their own little Scala module to access the PIDE infrastructure,
> and expose it to an existing Java program, if they really have to.

Exactly. If there are only a handful of different commands which need to
be supported, such a wrapper seems to be the best idea. But even then,
one needs to think about whether the interaction is supposed to be
asynchronous, because Java is lacking in that regard.

In order to start with a minimal solution, I'd like to bypass asynchronous interaction (which is no restriction on Isac's present solution).

First question: what is your experience with NetBeans versus Eclipse in projects combining Java and Scala?

Walther

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

On 14-11-21 09:51 AM, Lars Hupel wrote:
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.