Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] scala-isabelle: A library for interfacing with...


view this post on Zulip Email Gateway (Nov 12 2020 at 13:23):

From: Dominique Unruh <unruh@ut.ee>
Dear all,

I would like to announce my library scala-isabelle which is a library
for controlling and interacting with an Isabelle process from a Scala
application (or Java, ...). Some highlights:

* It enables fine-grained interactions (e.g., you can do pattern
matching and similar operations on individual terms in the Scala
application as if they were Scala types, but also apply Isabelle
operations (e.g., simplification) on it, transparently).
This means you can use it to build applications that reason about
math and use the existing Isabelle theories/tools for some
operations. (Such as the theorem prover qrhl-tool
<https://github.com/dominique-unruh/qrhl-tool>.)

* It is extensible: besides built in support for Isabelle objects such
as terms, contexts, theorems, ..., one can easily add support for
new types and operations without changing the library itself.

* Garbage collection is supported: Isabelle values can be garbage
collected when they are released in Scala.

* Speed: on my computer, the round-trip time for simple operations is
0.03ms, compared to ~20ms which seemed to be the round-trip time of
the PIDE-based libisabelle.

* It is supposed to be a replacement of the discontinued libisabelle
<https://github.com/larsrh/libisabelle> by Lars Hupel.

You can find more information in the README
<https://github.com/dominique-unruh/scala-isabelle/blob/master/README.md>.

Or ask me anything (especially if you are wondering whether
scala-isabelle is useful for your project or has specific features),
e.g., in the Gitter chat
<https://gitter.im/dominique-unruh/scala-isabelle> or by email.

Best wishes,
Dominique.


Last updated: Dec 05 2021 at 23:19 UTC