Email Gateway (Nov 09 2021 at 09:42): Email Gateway (Nov 09 2021 at 09:42):From: Dominique Unruh <unruh@ut.ee>
Hi,
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.)
I have a theory that contains a trivial lemma with smt-method (lemma
True by smt).
When I load this theory via Isabelle/Scala, I get the following exception:
exception Fail raised (line 57 of "System/isabelle_system.ML"): Bad
bash_process server address
At command "by" (line 6 of
"~/svn/qrhl-tool/scala-isabelle/src/test/isabelle/Theory_With_Smt.thy")
I initialize Isabelle roughly as follows:
Isabelle_System.init(isabelle_root = isabelleRoot.toString)
val channel = System_Channel()
val options = Options.init()
val channel_options = options.string.update("system_channel_address", channel.address).
string.update("system_channel_password", channel.password)
val sessionRoots2 = sessionRoots.map(p => isabelle.File.path(p.toFile)).toList
val sessions_structure = Sessions.load_structure(options = options, dirs = sessionRoots2)
val store = Sessions.store(options)
ML_Process(channel_options, sessions_structure, store, eval_main = mlCode, logic = logic, cwd = cwd.toFile)
Here mlCode is some ML code that does some communication and then
effectively runs the following code:
Thy_Info.use_thy (Path.implode path)
Thy_Info.get_theory name
where path and name are the path and name of the theory with the smt call.
The same above works fine with theories that do not contain smt.
I'm sorry not to provide a runnable example, but give the concrete
setup, it would be quite some work to cut everything down to a runnable
example. I'm hoping the issue can be clarified without one. But if not,
I can try to produce one.
Best wishes,
Dominique.
Email Gateway (Nov 09 2021 at 11:28):From: Makarius <makarius@sketis.net>
The relevant NEWS entry for Isabelle2021-1 is this:
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
Email Gateway (Nov 09 2021 at 11:42):From: Dominique Unruh <unruh@ut.ee>
Hi,
Email Gateway (Nov 09 2021 at 12:09):From: Makarius <makarius@sketis.net>
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
Email Gateway (Nov 09 2021 at 13:44):From: Dominique Unruh <unruh@ut.ee>
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
Email Gateway (Nov 09 2021 at 15:35):From: Makarius <makarius@sketis.net>
The Isabelle/PIDE server does have a lot of explicit documentation: chapter 4
of the "system" manual. In retrospect, I am unsure if it ever got used in
applications so far.
There is a report by Boris Shminke on using it from Python:
https://link.springer.com/chapter/10.1007%2F978-3-030-81097-9_20 --- but it
remains unclear if and how it works in applications.
Makarius
Email Gateway (Nov 10 2021 at 20:01):From: Simon Wimmer <wimmersimon@gmail.com>
We have another application for grading Isabelle theories on
do.proof.in.tum.de:
https://github.com/maxhaslbeck/proving-contest-backends/blob/master/Isabelle/grader.py
Simon
Last updated: Jul 15 2022 at 23:21 UTC