Re: [isabelle] replace "isabelle tty"



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>





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