Re: [isabelle] Isabelle2021-1-RC2: Exception when initializing services



> Yes, we've had long discussions about the obsolete scala-isabelle library already.

I would disagree that it is obsolete.

At least not in the sense that there is a different approach that covers the same needs, to my knowledge.

The core Isabelle framework, as far as I can tell, covers the following use cases well:

What is not supported (as far as I can tell) is:

If there is a mechanism that covers those things, then I'd be happy to use that mechanism. (Ideally, scala-isabelle would be nothing than a simpler to use helper library that just passes through everything to Isabelle/Scala.)

I'm also happy to use the "proper way" of invoking Isabelle inside the library.

(Note that, if I wouldn't use the library, I would still have exactly the same problems because in the qrhl-tool theorem prover, I need to invoke Isabelle, and if I do it by calling Isabelle/Scala directly, I will still have exactly the same questions.)

Best wishes,
Dominique.


On 11/9/21 1:16 PM, Makarius wrote:
On 09/11/2021 12:09, Dominique Unruh wrote:

        
Note that the isabelle.setup module is a step towards better integration (or
assimilation) of Java/Scala into Isabelle (not Isabelle into Java/Scala).
There will be further steps after the coming release, e.g. jars as exports
within the session database --- e.g. for services that build the document.
My use case is the opposite direction. I use Isabelle/Scala to create an
instance of Isabelle (in the scala-isabelle library). Originally, I invoked
Isabelle via command line inside the library, but following your suggestion
this spring or so (and also because invoking things on the command line in
Windows led to a lot of brittleness with bash/cygwin-versions and command line
quoting etc.) I replaced it by an invocation of Isabelle using Isabelle/Scala.
Yes, we've had long discussions about the obsolete scala-isabelle library already.

The more Java/Scala gets assimilated into Isabelle, the less it will work as
in the old times.

Rather soon, I hope to see a proper Scala IDE inside PIDE: Scala 3 might open
this possibility.


	Makarius



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