Re: [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)



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




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