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



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.