Email Gateway (Aug 19 2022 at 16:25): Email Gateway (Aug 19 2022 at 16:25):From: Walther Neuper <wneuper@ist.tugraz.at>
Hi Lars,
with great interest I studied your code [1] (cited below), followed the
function calls into /src/Pure/System, /src/Pure/PIDE etc and tried
to understand.
So far I understood, that
(1) Session.protocol_handler starts a persistent session
(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.
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).
Could you, please, help once more?
Walther
Email Gateway (Aug 19 2022 at 16:25):From: Lars Hupel <hupel@in.tum.de>
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
Email Gateway (Aug 19 2022 at 16:25):From: Makarius <makarius@sketis.net>
On Fri, 21 Nov 2014, Lars Hupel wrote:
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).
Isabelle/Scala is indeed the main system programming language for
Isabelle, so the manual should say more about it. The reason why so
little Isabelle/Scala is in the manuals is that code snippets cannot be
formally checked, as is done for Isabelle/ML. Without formal checking, it
is pointless to make examples, because they will stop working in no time,
after the next round of refinements of the system implementation.
I reckon that with the removal of "isabelle tty", more applications of
Isabelle/Scala will emerge.
Probably yes, and for two reasons:
(1) Without the TTY baggage it becomes more feasible to introduce formal
Isabelle/Scala checking in the documentation, in the sense above.
(2) Removal of obsolete things makes people active, who are still using
very old archeological layers of the system. Actual use of new
programming interfaces always helps to make them more smooth and
easier to use.
The Isabelle process protocol concepts covered here are in fact already
quite well-established and polished for some years. So now is the right
time to convert old applications, and to forget that there was ever a TTY
loop in Isabelle.
Makarius
http://stop-ttip.org 925,281 people so far
Email Gateway (Aug 19 2022 at 16:26):From: Lars Hupel <hupel@in.tum.de>
Indeed.
What could be done is writing a minimal PIDE application demonstrating
bi-directional communication, possibly in the style of literate
programming. This could then be executed and tested as part of a regular
(nightly?) build against the repository version.
Cheers
Lars
Email Gateway (Aug 19 2022 at 16:26):From: Cezary Kaliszyk <cezarykaliszyk@gmail.com>
Dear Walther,
There is also a different approach to simulating the TTY/ProofGeneral
interaction with Isabelle.
I have written a small 20-line script that lets me imitate
minimal Isar-interaction via isabelle-console. It only allows
sending single lines to Isabelle, there is no "back" or error
handling, but this is enough for simple sending of commands to
Isabelle and analysing their outputs.
The reason why I use this script, is because I use Isabelle
on a headless server. It has enough memory to do bigger
experiments, but I cannot run graphical applications there,
in particular I cannot run PIDE. As ProofGeneral and TTY
support have been removed, I needed to implement some minimal
interaction, and the minimum, following the indispensable
help from Makarius is:
The script runs:
"isabelle console",
Then sends it:
"val s = Toplevel.toplevel;"
And for every line of user input sends:
"val s = fold (Toplevel.command_exception true) (Outer_Syntax.parse
Position.start \"%s\") s;"
I suppose this could be extended to support a "go-back" or even
some more complicated protocol like the one from ProofGeneral
which I presume you are currently using.
Attached, sorry for yet another programming language, but the
above should explain it.
Regards,
Cezary
isatty.ml
Email Gateway (Aug 19 2022 at 16:26):From: Walther Neuper <wneuper@ist.tugraz.at>
Dear Cezary,
thank you for the surprising mini-solution ...
... we have an even simpler protocol than ProofGeneral, so your solution
would be quite appropriate for a quick shortcut.
Such a shortcut would be necessary, if the efforts required for a
solution via Isabelle/Scala would be beyond our present resources.
So, probably we come back to your solution after some trials.
Regards,
Walther
Email Gateway (Aug 19 2022 at 16:26):From: Walther Neuper <wneuper@ist.tugraz.at>
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 JavaThe 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
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
Email Gateway (Aug 19 2022 at 16:28):From: Makarius <makarius@sketis.net>
The problem posed here is technically trivial, i.e. a non-problem. It is
just a matter to overcome old ways of thinking about it.
Isabelle/Scala is well-established as the main system programming
interface for several years. When you want to connect to some Isabelle
prover process, the Scala APIs are the way to do it.
Pretty soon, it will be no longer possible to use the Isabelle process at
all, without the Scala process around it. The remaining TTY loop was
hindering important reforms long enough. After Isabelle2014 it is no
longer there, without any traces of it left.
Then it becomes possible to assume that things like Invoke_Scala.method
work in Isabelle/ML all the time, and many problems from the past can be
resolved in the proper way. (E.g. a brushed-up version of document
preparation.)
Makarius
http://stop-ttip.org 927,487 people so far
Email Gateway (Aug 19 2022 at 16:28):From: Makarius <makarius@sketis.net>
On Fri, 21 Nov 2014, Walther Neuper wrote:
In order to start with a minimal solution, I'd like to bypass
asynchronous interaction (which is no restriction on Isac's present
solution).
Asynchronous interaction is already the minimal solution. It is simpler
than synchronous interaction in many ways.
Just give up the notion that you are mutating an implicit "current state".
You can easily pass around explicit handles to immutable values that are
bounced back and forth between the ML and Scala process in an asynchronous
manner.
The application by Lars demonstrates that nicely.
First question: what is your experience with NetBeans versus Eclipse in
projects combining Java and Scala?
The current high-end IDE is probably IntelliJ IDEA, but I am using myself
just jEdit as plain text editor for Scala.
Makarius
http://stop-ttip.org 927,491 people so far
Email Gateway (Aug 19 2022 at 16:28):From: Lars Hupel <hupel@in.tum.de>
First question: what is your experience with NetBeans versus Eclipse in
projects combining Java and Scala?
Last time I used NetBeans with Scala was in 2010. It was quite unstable,
and when I revisited it a couple of months ago, the situation has not
improved significantly.
IntelliJ is good, but implements its own type checker for Scala which
may or may not agree with the official Scala compiler. I found its "type
aware" highlighting annoying to use because of spurious error markers.
The recommended IDE to use with Scala/Java is Eclipse. It is
commercially supported from Typesafe and should be stable enough. I
don't have practical experience with it, though.
Email Gateway (Aug 19 2022 at 16:28):From: Makarius <makarius@sketis.net>
Concerning the general topic of the relation Isabelle/Scala/PIDE vs. the
now removed TTY / Proof General interaction mode, see also this blog entry
of mine: http://sketis.net/2014/discontinuation-of-isabelle-proof-general
Makarius
http://stop-ttip.org 935,236 people so far
Email Gateway (Aug 19 2022 at 16:41):From: Walther Neuper <wneuper@ist.tugraz.at>
We did not engage for "Remaining uses of Proof General" because we hope
for easy ways to replace "isabelle tty" in our prototype, and because we
look forward to replace our self-made front-end by Isabelle/jEdit as
soon as Isabelle goes collaboration and includes session management.
Until Isabelle2013-2, our prototype had the communication between its
front-end (client) in Java and its mathematics-engine (server) in
Isabelle/ML via stdin/stdout of the server process:
(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"
(c) the client requests were ML functions f : a1 -> .. -> an -> unit
written to stdin as text "ML {* f a1 .. an *}"
(d) the functions f wrote data in XML-format, which was read from stdout
by a Java XML parser.
We want to invest into replacement of this outdated communication the
more, the closer Isabelle comes to a session management. So presently
our questions are
(1) Is the code around the removed "isabelle tty" already stable enough
to start replacement of "isabelle tty" in our project now ?
(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 ?
We are aware, that the above questions are at the borderline of this
mailing list's scope --- so we are really grateful for any help!
Walther
[1] http://www.ist.tugraz.at/isac
Email Gateway (Aug 19 2022 at 16:41):From: Lars Hupel <hupel@in.tum.de>
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
Email Gateway (Aug 19 2022 at 16:41):From: Makarius <makarius@sketis.net>
That is the old question of accessing a Scala library from Java.
You probably understand yourself more about the Scala compiler and its
representation of Scala things on the JVM than I do. 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.
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. In some
sense, Isabelle/jEdit does the same, because jEdit is just another Java
program.
Big commercial frameworks like Akka advertize dual Java and Scala APIs,
but that is not for free -- it was implemented like that from the start
(with the intention to make money in the Java market).
Makarius
http://stop-ttip.org 909,835 people so far
Email Gateway (Aug 19 2022 at 16:41):From: Lars Hupel <hupel@in.tum.de>
You probably understand yourself more about the Scala compiler and its
representation of Scala things on the JVM than I do. 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.
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. In
some sense, Isabelle/jEdit does the same, because jEdit is just another
Java program.
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.
Lars
Email Gateway (Aug 19 2022 at 16:41):From: Walther Neuper <wneuper@ist.tugraz.at>
thanks a lot for the quick replies!
(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.
Very good. so let's start.
(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.
Right.
Our protocol is very primitive, it is NOT asynchronous:
(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?
The set of functions f is fixed and cannot be expanded by the user,
https://intra.ist.tugraz.at/hg/isa/file/c06c18fe06e0/src/Tools/isac/Frontend/interface.sml#l10.
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.
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.
So I'll go to study [1,2].
My hope is still, to stay within Java, because you say
The only guarantee is calling Java from Scala, and even that
breaks from time to time because of mismatches between their type systems.
Thanks a lot,
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>
Last updated: Nov 21 2024 at 12:39 UTC