Email Gateway (Aug 22 2022 at 17:01): Email Gateway (Aug 22 2022 at 17:01):From: Makarius <makarius@sketis.net>
Dear Isabelle users,
please see this blog post on the new Isabelle server:
https://sketis.net/2018/the-isabelle-server-responsive-control-of-prover-sessions
It should already be usable, although there are no users yet.
In the coming months before the Isabelle2018 release, it should become
really robust and stable, but that requires feedback from applications
to get there.
Makarius
Email Gateway (Aug 22 2022 at 17:02):From: Walther Neuper <wneuper@ist.tugraz.at>
Our application
https://intra.ist.tugraz.at/hg/isa
https://intra.ist.tugraz.at/hg/isac
(server and client respectively) uses libisabelle
https://github.com/larsrh/libisabelle
to connect Isabelle with our Java/Scala front-end. This connection is
reliable and well maintained over Isabelle versions.
If I understand correctly from a quick review of the material pointed at
above, then the new Isabelle server would allow to replace libisabelle
with little effort and open new prospects for further development of our
application.
So we would be interested to invest the efforts required. However, we
would probably need some help, since we have no expert in our team to
deal with intricacies of TCP/IP etc presently.
Walther
Email Gateway (Aug 22 2022 at 17:02):From: Makarius <makarius@sketis.net>
On 29/03/18 11:58, Walther Neuper wrote:
Our application
https://intra.ist.tugraz.at/hg/isa
https://intra.ist.tugraz.at/hg/isac
(server and client respectively) uses libisabelle
https://github.com/larsrh/libisabelle
to connect Isabelle with our Java/Scala front-end. This connection is
reliable and well maintained over Isabelle versions.If I understand correctly from a quick review of the material pointed at
above, then the new Isabelle server would allow to replace libisabelle
with little effort and open new prospects for further development of our
application.
I can't say much about libisabelle: I've read the sources 2-3 times,
without really understanding how it works and what it does. My general
impression is that it connects to a raw toplevel environment without
PIDE document context.
The point of the new Isabelle Server (which was already planned in
2009/2010 but only now implemented) is to have a "headless" PIDE
connection. I.e. some other program throws theory sources declaratively
at the server and gets feedback according to the built-in policies (e.g.
for parallel checking).
So we would be interested to invest the efforts required. However, we
would probably need some help, since we have no expert in our team to
deal with intricacies of TCP/IP etc presently.
You do not have to understand TCP/IP. Connecting to a server e.g. on the
JVM is trivial, you merely open the socket like this (with the port
reported by the "isabelle server" tool):
$ isabelle scala
import java.net.{Socket, InetAddress}
val socket = new Socket(InetAddress.getByName("127.0.0.1"), port)
Now you can read/write over the socket byte channels as usual. Here is
the most primitive example (with the password reported by the "isabelle
server" tool):
import isabelle._
socket.getOutputStream.write(UTF8.bytes(password + "\n"))
socket.getOutputStream.flush()
socket.getInputStream.read()
socket.getInputStream.read()
socket.getInputStream.read()
The latter should give "OK ", i.e. 79, 75, 32 (the response is actually
a bit longer).
The remaining work is to read and write messages in the format described
in chapter 4 of the "system" manual. It also involves JSON syntax.
If you are already on the JVM platform, you can bypass the server and
use the library functions for Scala (not Java) directly. E.g. like this:
$ isabelle scala
val options = Options.init()
val session = Thy_Resources.start_session(options, "HOL", progress =
new Console_Progress)
val result = session.use_theories(List("~~/src/HOL/ex/Seq"), progress
= new Console_Progress)
Then you can inspect result.nodes, result.messages(node_name) etc. -- it
provides a representation that is closer to PIDE, while the server
imitates command-line output, see also
http://isabelle.in.tum.de/repos/isabelle/annotate/ad735a551a11/src/Pure/Tools/server_commands.scala#l200
Makarius
Email Gateway (Aug 22 2022 at 17:02):From: Lars Hupel <hupel@in.tum.de>
The main purpose of libisabelle is to offer a uniform,
version-independent way to put Isabelle under library control, as
opposed to the usual model of Isabelle controlling other tools. The
features supported are informed by wanting Isabelle (and the AFP) to be
just another JAR file that your application can link to.
If you don't need that, the existing tooling also allows you to manage
Isabelle installations on your local machine, sort of like a package
manager. But that's about it. libisabelle has no notion of networks, nor
does it try to reimplement Isabelle features.
Lars
Last updated: Apr 26 2024 at 20:16 UTC