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



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.




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