Email Gateway (Feb 09 2021 at 18:35): Email Gateway (Feb 09 2021 at 18:35):From: Dominique Unruh <unruh@ut.ee>
Hi,
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.
Email Gateway (Feb 09 2021 at 19:33):From: Makarius <makarius@sketis.net>
On 09/02/2021 19:34, Dominique Unruh wrote:
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.
Exactly. Over 10 years I have given many talks and written many papers about
Isabelle/Scala in contrast to Isabelle/ML. The main idea:
* Isabelle/Scala is for systems-programming / system integration
* Isabelle/ML is for mathematical logic
Sometimes there is a bit of overlap, and some freedom to decide where things
happen. But when you start to do term operations in Isabelle/Scala it is
probably wrong.
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.)
So why not do this in Isabelle/ML? It works much better. E.g. you have proper
antiquotations for the const name "HOL.Trueprop" above --- without that it is
not going to last very long.
Why give up static scopes and types by pretending that ML operations can
happen in Scala?
(And of course, this is extensible by ML code fragments in the Scala program.)
The proper way is to define Isabelle/Isar commands in Isabelle/ML, and let the
Isabelle/Scala front-end work in a high-level way with it.
Chapter 4 of the "system" manual describes a fairly simple and declarative
server protocol to work with Isabelle documents: the socket-version works via
JSON (e.g. for Python), but it is easier to work with the same in
Isabelle/Scala (the Headless PIDE session).
Makarius
Email Gateway (Feb 09 2021 at 20:19):From: Makarius <makarius@sketis.net>
Some further side-remarks specifically for Isabelle2021 (see NEWS):
Various examples may be found by using Isabelle/jEdit hypersearch for the text
"isabelle_scala_service" within all "settings" files in the $ISABELLE_HOME
directory (and all subdirectories).
An alternative is to search for class instances of "Isabelle_System.Service"
in *.scala files within $ISABELLE_HOME.
As an abstract example, a user-defined Isabelle/Scala module could register
its own command-line tools or Isabelle server commands (for JSON access). The
Scala implementation does the main system integration; if some mathematical
logic is required, it will be done in an auxiliary theory context for the tool
(e.g. embedded ML files to define Isar commands).
As a concrete example, consider Isabelle/Naproche in Isabelle2021-RC5. Follow
the Documentation pointer to $ISABELLE_NAPROCHE/Ex.thy --- it contains some
hints about the implementation at the bottom. Apart from Isabelle/ML and
Isabelle/Scala, this involves another program implemented in Haskell. The
latter uses Isabelle/Haskell library for basic communication with
Isabelle/PIDE (even with properly checked antiquotations instead of freely
invented string literals).
Makarius
Email Gateway (Feb 11 2021 at 11:55):From: Dominique Unruh <unruh@ut.ee>
Exactly. Over 10 years I have given many talks and written many papers about
Isabelle/Scala in contrast to Isabelle/ML. The main idea:* Isabelle/Scala is for systems-programming / system integration
* Isabelle/ML is for mathematical logic
Sometimes there is a bit of overlap, and some freedom to decide where things
happen. But when you start to do term operations in Isabelle/Scala it is
probably wrong.
Good. Then I got things right. So we have a clear separation of purposes
between Isabelle/Scala and scala-isabelle.
*
Isabelle/Scala is for systems-programming / system integration
*
Isabelle/ML is for mathematical logic
* scala-isabelle is also for mathematical logic (and for any other
more low-level inspection of Isabelle data)
Anythings that can be done in scala-isabelle can also be done in
Isabelle/ML, of course. (And vice versa.) However, if due to the
constraints of the project, we want to use Scala (or any other JVM
language), then scala-isabelle would be the right choice.
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.)
So why not do this in Isabelle/ML? It works much better. E.g. you have proper
antiquotations for the const name "HOL.Trueprop" above --- without that it is
not going to last very long.
There can be several reasons (it depends on the project):
* We use Isabelle as part of a bigger application (e.g., I developed
the qrhl-tool theorem prover in Scala, and it uses Isabelle as a
component for reasoning about verification conditions).
* Scala is easier to debug and edit with modern IDEs. Isabelle/ML has
some support (e.g., ctrl-click is useful), but imho it does not come
close to the tool support that we have in modern IDEs.
* I want integration with GUI components. (E.g., I could imagine some
tool to interactively explore the structure of terms. This would be
possible with Isabelle/Scala, I think, but I would have to serialize
all possibly relevant information about the terms, send them over in
a bunch, and then deserialize them. Lots of boilerplate.)
About the antiquotation: This was just an illustrative example. You can
also use antiquotations in Scala, so you could write something like
/term match { case term"?x ==> Trueprop ?y" => print(x); print(y) }/.
Why give up static scopes and types by pretending that ML operations can
happen in Scala?
Since Scala has a rich type system on its own, there is no need to give
up on those things. ML types can be mirrored on the Scala side.
Best wishes,
Dominique.
Email Gateway (Feb 11 2021 at 13:22):From: Makarius <makarius@sketis.net>
On 11/02/2021 12:53, Dominique Unruh wrote:
Exactly. Over 10 years I have given many talks and written many papers about
Isabelle/Scala in contrast to Isabelle/ML. The main idea:* Isabelle/Scala is for systems-programming / system integration
* Isabelle/ML is for mathematical logic
Sometimes there is a bit of overlap, and some freedom to decide where things
happen. But when you start to do term operations in Isabelle/Scala it is
probably wrong.Good. Then I got things right. So we have a clear separation of purposes
between Isabelle/Scala and scala-isabelle.*
Isabelle/Scala is for systems-programming / system integration
*
Isabelle/ML is for mathematical logic
* scala-isabelle is also for mathematical logic (and for any other more
low-level inspection of Isabelle data)Anythings that can be done in scala-isabelle can also be done in Isabelle/ML,
of course. (And vice versa.) However, if due to the constraints of the
project, we want to use Scala (or any other JVM language), then scala-isabelle
would be the right choice.
The choice is up to you. Within the regular Isabelle ecosystem, the proper
language for heavy-duty symbolic logic is Isabelle/ML: it has been made
precisely for that over 35 years. We could not crunch the great things in AFP
without Isabelle/ML as it is today.
To conclude this overview of possibilities, here is a further NEWS entry from
Isabelle2021:
* ML *
This means that Isabelle/ML programs can appeal to operations in Scala, if
that happens to be available on that side, e.g. for historical reaans or
existing Java implementations. Thus the order of control is straight-forward:
ML hands over to Scala like a regular function call, without any special
programming tricks exposed outside.
An example application is Nitpick/Kodkod, which works either as a heavy JVM
process or light Scala thread (both invoked from Isabelle/ML):
Side-remark: Originally I wanted to get rid of the JVM process for
Isabelle2021, but this has to wait for the next release, due to remaining
assumptions in the Kodkod implementation concerning the Java context
(interrupts, threads, exit).
Scala is easier to debug and edit with
modern IDEs. Isabelle/ML has some support
(e.g., ctrl-click is useful), but imho it
does not come close to the tool support
that we have in modern IDEs.
The term "modern" sounds very old-fashioned to me. Modern times have ended
some decades ago; we now have the post-modern era.
For Isabelle projects, the Isabelle Prover IDE has very good integration of
everything: Isar, ML, other sub-languages. I know this best and like this
best. It is also quite easy to integrate your own sub-languages with PIDE
support (implemented all in Isabelle/ML).
Isabelle/Scala is an exception: it is not (yet?) integrated into
Isabelle/PIDE, but the "isabelle scala_project" tool allows to generate a
Gradle project for use in IntelliJ IDEA: I do like that IDE, but that alone
would never be a reason to disregard our fine Isabelle/ML working environment.
VSCode is another popular quasi-IDE option: Isabelle/VSCode is a minimal
experiment, much more could be done. Generally, I see a lot of IDE concepts
retrofitted into the VSCode editor project, but it might require 5-10 more
years to become a proper IDE.
Makarius
Last updated: Apr 19 2024 at 16:20 UTC