Email Gateway (Aug 22 2022 at 11:07): Email Gateway (Aug 22 2022 at 11:07):From: Walther Neuper <wneuper@ist.tugraz.at>
On 2015-08-11 18:20, Lars Hupel wrote:
questions:
(1) As you say, libisabelle is dedicated to "non-IDE applications" So
the synchronous Protocol makes sense. However, Isac is designed for an
asynchronous communication between Java frontend and the Isabelle/Isac
backend -- what are the obstacles to have libisabelle with asynchronous
communication?
It is completely asynchronous internally. It uses a concept of "futures"
which is available in both ML [*] and Scala []. Simply speaking,
whenever a new operation is invoked from Scala, it is sent to the prover
asynchronously and processed by some thread in a worker farm.Could you describe how the asynchronous communication worked previously in
Isac?
The Isac Java front-end has lots of different methods addressing the
Math_Engine in Isabelle/Isac [1] and only one kind of reply announcing
"the calculation has been changed successfully" [2] (or an error
message); and then the front-end is free to request further data from
the Math_Engine as required.
However, since we used "isabelle tty" so far, this asynchronous design
did not yet come into effect due to the synchronous nature of
stdin/stdout (which we found out only after the design phase).
Isabelle2015 support is there (for the Scala API), I just need to figure
out how to reconstruct Java support without breaking the previous API
much.
This sounds great; we'd appreciate to see Isac's initial asynchronous
design at work.
Walther
[1] Java-side:
https://intra.ist.tugraz.at/hg/isac/file/32f5e8e1c538/isac-java/src/java/isac/interfaces/IToCalc.java
ML-side:
https://intra.ist.tugraz.at/hg/isa/file/f323be267fa2/src/Tools/isac/Frontend/interface.sml
[2]
https://intra.ist.tugraz.at/hg/isac/file/32f5e8e1c538/isac-java/src/java/isac/interfaces/IToUser.java
[*] See the introductory paragraphs in
<http://docs.scala-lang.org/sips/completed/futures-promises.html>
[**] Sec 3.1 in<http://www4.in.tum.de/~wenzelm/papers/itp-smp.pdf>
Last updated: Apr 26 2024 at 20:16 UTC