[isabelle] Comparing Isabelle/Scala with scala-isabelle. Was: Isabelle code for getting in-memory representation (abstract syntax trees) for complete theory file (tree of loaded theories)



Hi,


For serious and robust development, I, too, believe the Isabelle/Scala
interface is the best option. Dominique’s scala-isabelle library
(https://github.com/dominique-unruh/scala-isabelle) could be of great use.
I still don't understand the purpose of it.

Why not use Isabelle/Scala directly, it is an integral part of Isabelle?

I cannot fully answer that question because I was not able to find the documentation of Isabelle/Scala.

(Only the one in the system manual, which did not make clear to me what Isabelle/Scala supports.)

My impression of Isabelle/Scala is that it focuses a lot on the high-level operations (theory management, builds, etc.) but does not have support for operating on lower-level data.

For example, in scala-isabelle, you can directly and transparently work on terms, cterms, thms, etc. (For example, I can do something like "thm.proposition match { case Const("HOL.Trueprop", t) => do something with term t }". (And references on the scala side to Isabelle values can get automatically garbage collected etc.)

(And of course, this is extensible by ML code fragments in the Scala program.)

Of course, assuming that Isabelle/Scala allows to transfer data (e.g., XML trees) between Scala and Isabelle, and that it allows to execute ML code, it would be possible to do all those things also with Isabelle/Scala. But the question is whether that support is part of Isabelle/Scala, or is something that can be hypothetically implemented. The basic invocation and communication between Scala and Isabelle is just 1k LOC in scala-isabelle, so that's the smallest part of it.

In fact, I think that it would be easy to base scala-isabelle on a different communication protocol, e.g., Isabelle/Scala. However, I opted to make a simple lowlevel protocol instead because that way I got a factor 1000 improvement in roundtrip time over what Lars Hupel's libisabelle has. (And afaik, libisabelle was built on top of Isabelle/PIDE, not sure how this relates to Isabelle/Scala.)

That being said, I think it should not be hard to refactor scala-isabelle so that one can choose whether to use Scala/Isabelle or my own protocol for the communication.

All of this, of course, is under the assumption that I my guesses are right about what Isabelle/Scala does.

I would be happy if you can elucidate me as to what the purpose of Isabelle/Scala is, and what features it has.

Best wishes,
Dominique.








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