Re: [isabelle] Isabelle2021-1-RC2: Invoking smt-method in theory loaded via Isabelle/Scala



Hi,

You can see in Isabelle/jEdit and Isabelle/VSCode how the Session objects are
created and initalized.
OK, I will try and reverse engineer from there.

You should actually try to dismantle scala-isabelle. It has caused enough
tensions and continuous problems in the past.
I think there is a misunderstanding here.

If I dismantle scala-isabelle, I will still have to invoke Isabelle from within qrhl-tool (unless you suggest to dismantle that theorem prover, too).  (Unless you count the repeated mails some time ago where someone insisted in using scala-isabelle for getting an AST of an Isabelle theory despite your and my explanations that this is not supported by Isabelle or scala-isabelle.)

And the difficulties I have raised in this list related to scala-isabelle are due to the fact that it is not clear (to me) and also somewhat in flux, how to invoke Isabelle from Scala.

So I would have exactly the same questions if I would not use scala-isabelle.

scala-isabelle actually makes things easier because it encapsulates the undocumented (or documented-by-source-code) aspects of the invocation of Isabelle into a documented API (that also changes less).

Best wishes,
Dominique.






On 11/9/21 2:08 PM, Makarius wrote:
On 09/11/2021 12:40, Dominique Unruh wrote:
We have already had long discussions about remaining possibilities to run
Isabelle without a proper PIDE session context.
Yes, and you convinced me not to do that. The code fragment in my mail was my
attempt to programmatically initialize such a PIDE session context. However, I
do not know what a "proper PIDE session context" means in terms of the methods
that I invoke. I thought Isabelle.init followed by ML_Process would do that.
Should I initialize it differently?
The PIDE session object in my snippet is this:

   val session = new Session(options, Resources.empty)

But that is not quite "proper": the resources are empty and it is not
connected to an ML process. The Bash.Handler does not care right now.


Note that I don't directly care about the bash, it just happens that the
exception I got related to bash, but what I needed was to invoke "by smt".
There are two assumptions behind that:

   * bash_process works (this thread)

   * z3 works: it has always been somewhat fragile and is de-facto downgraded
now; veriT takes more and more over.


So I don't want to do low-level tinkering if it can be avoided, but correctly
initialize PIDE (as long as this can be done starting the Isabelle process
from Scala, as opposed to the other way around).
You can see in Isabelle/jEdit and Isabelle/VSCode how the Session objects are
created and initalized. The scala_project Maven project makes it very easy to
browse the implementation.


My goal is to have scala-isabelle use the officially supported ways to get
maximum stability.
You should actually try to dismantle scala-isabelle. It has caused enough
tensions and continuous problems in the past.


	Makarius




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