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



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.