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



Hi,

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?

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".

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).

My goal is to have scala-isabelle use the officially supported ways to get maximum stability.

Best wishes,
Dominique.



On 11/9/21 1:28 PM, Makarius wrote:
On 09/11/2021 10:41, Dominique Unruh wrote:
I have one problem with an Isabelle/Scala initialized Isabelle session. I do
not know whether this indicates a regression or is because I initialize
Isabelle wrongly. (The problem did not occur with Isabelle2021.)
The relevant NEWS entry for Isabelle2021-1 is this:

* External bash processes are always managed by Isabelle/Scala, in
contrast to Isabelle2021 where this was only done for macOS on Apple
Silicon.

The main Isabelle/ML interface is Isabelle_System.bash_process with
result type Process_Result.T (resembling class Process_Result in Scala);
derived operations Isabelle_System.bash and Isabelle_System.bash_output
provide similar functionality as before. The underlying TCP/IP server
within Isabelle/Scala is available to other programming languages as
well, notably Isabelle/Haskell.


We have already had long discussions about remaining possibilities to run
Isabelle without a proper PIDE session context.

Many system operations already use the Isabelle/Scala function protocol, e.g.
Isabelle_System.make_directory. This works much better and more portably that
e.g. perl in the past (perl has been discontinued altogether for Isabelle2021-1).

For "bash_process" there is something special: the service is actually via
TCP, e.g. to allow Haskell (or eventually OCaml) to run the external process
in the Isabelle way.

Thus you merely need a proper server in Isabelle/Scala + options for
Isabelle/ML, and not a full PIDE session.  Here is an example of such
low-level tinkering that could work by accident:


import isabelle._

val options = Options.init()
val session = new Session(options, Resources.empty)
val bash_handler = new Bash.Handler
bash_handler.init(session)

val ml_options = bash_handler.prover_options(options)

// sanity check:
ml_options.string("bash_process_address")
ml_options.string("bash_process_password")

// run ML_Process
ML_Process(ml_options, ...)

bash_handler.exit()


	Makarius




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