Re: [isabelle] scala interface



On Fri, 17 Feb 2012, Matthias Schmalz wrote:

I am trying to use the scala library Pure.jar to communicate with the Isabelle process. A typical use case is to send a theory snipped like the following and to check whether the proof attempt succeeds:

theory Test imports Main begin

lemma foo:
fixes x :: bool
assumes "x = True"
shows "x | x"
using assms
by simp

I have already discovered the Isabelle_System.init method and I am aware of the classes "Isabelle_Process" and "Session". My attempts to communicate the above snippet to an Isabelle_Process failed due to my unawareness of the input format of Isabelle_Process.input. (Perhaps, this is not the intended interface anyway?) I also tried to use Session.init_node, but I am not sure how to choose the parameters and how to receive the result.

First let's fix the Isabelle version for this thread: the latest release Isabelle2011-1. It does not make sense to use an older Isabelle version with Isabelle/Scala, due to the many substantial improvements of the same that went into Isabelle2011-1.


Direct use of Isabelle_Process.input connects you with the protocol interpreter on the other side. It is theoretically possible to extend its set of protocol commands in user space, but that would mean to produce your own protocol implementation, which is a bit challenging to get really right.

It is better to use the official Isabelle/Scala document model, even though its API in Isabelle2011-1 is still a bit rough, and there are more details of the mechanics of the underlying interaction model still visible than I would like to have after 4 years working on that.


Attached is an example for doing the initial startup of the session together with the theory context; see also https://bitbucket.org/pide/pide_examples/src/2a4cfab96b3e/ex.scala (that repository might evolve further).

This is how to build and run it with Isabelle2011-1:

  shell> isabelle scalac ex.scala
  shell> isabelle scala
  scala> val session = PIDE_examples.Ex.Theory_Session()

The Theory_Session.apply() function has some further optional arguments; e.g. verbose = true gives you all the low-level protocol messages.

What makes the implementation a bit delicate is the bias of Session towards the current main application in the Isabelle/jEdit Prover IDE. Here the user throws edits at the prover, which in turn answers them incrementally in an fully asynchronous manner. There is never a point where a finished execution of some command transaction is enforced. I have recovered the latter in the above Theory_Session for the first half of the problem: prover startup and processing the theory header.

So you will get synchrous errors on the command line if anything fails here, say giving a bad logic image or imports. If you have your own GUI, you might reconsider asynchronous startup, see also ~~/src/Tools/jEdit/src/plugin.scala which should give an idea about the specific wiring with the main jEdit event bus.

What is still missing in the above ex.scala is the part about emitting the statement and proof, and inspecting its results. This requires some extra care due to potential non-termination of that part of the document.

We can discuss in further detail what your application really requires.


	Makarius
package PIDE_examples


import isabelle._

import scala.actors.Actor._


object Ex
{
  object Theory_Session
  {
    def apply(
      logic: String = "",
      imports: List[String] = List("Main"),
      verbose: Boolean = false): Theory_Session =
    {
      Isabelle_System.init()

      val logic1 =
        if (logic != null && logic != "") logic
        else Isabelle_System.getenv_strict("ISABELLE_LOGIC")

      new Theory_Session(logic1, imports, verbose)
    }
  }

  class Theory_Session private(logic: String, imports: List[String], verbose: Boolean)
    extends Session()
  {
    override val output_delay = Time.seconds(0.01)
    override val prune_size = 1  // number of old document versions to retain


    /* theory node */

    private val theory_name = "Theory"

    private val node_name =
    {
      val id = Document.new_id().toString
      val path = Thy_Header.thy_path(Path.root + Path.basic("dummy" + id) + Path.basic(theory_name))
      Document.Node.Name(path)
    }
    private val header_text: String =
      "theory " + quote(theory_name) + " imports " + imports.map(quote).mkString(" ") + " begin\n"
    private val header: Document.Node_Header = Exn.Res(Thy_Header.read(header_text))
    private val perspective = Text.Perspective(List(Text.Range(0, Integer.MAX_VALUE)))


    /* main actor */

    private case object Get_Startup
    private case object Get_Theory

    private val main_actor = actor {
      var startup_result: Option[Exn.Result[Unit]] = None
      var theory_result: Option[Exn.Result[Unit]] = None

      loop {
        react {
          case message: Isabelle_Process.Message =>
            System.err.println(message.toString)

          case phase: Session.Phase =>
            phase match {
              case Session.Failed =>
                startup_result =
                  Some(Exn.Exn(ERROR("Failed to start Isabelle process:\n" + syslog)))

              case Session.Ready =>
                startup_result = Some(Exn.Res(()))

              case Session.Shutdown =>  // FIXME

              case _ =>
            }

          case _: Session.Commands_Changed =>
            if (!theory_result.isDefined) {
              val snapshot = this.snapshot(node_name, Nil)
              if (!snapshot.is_outdated) {
                snapshot.node.commands.find(_.name == "theory").map(snapshot.command_state) match {
                  case None =>
                  case Some(state) =>
                    val err =
                      (for ((_, t) <- state.results.iterator; if Isar_Document.is_error(t))
                        yield Pretty.string_of(List(t))).mkString("\n")

                    Isar_Document.command_status(state.status) match {
                      case Isar_Document.Finished =>
                        theory_result = Some(if (err == "") Exn.Res(()) else Exn.Exn(ERROR(err)))

                      case Isar_Document.Failed =>
                        theory_result = Some(Exn.Exn(ERROR(err)))

                      case _ =>
                    }
                }
              }
            }

          case Get_Startup if startup_result.isDefined => reply(startup_result.get)

          case Get_Theory if theory_result.isDefined => reply(theory_result.get)

          case bad if startup_result.isDefined && theory_result.isDefined =>
            System.err.println("main_actor: ignoring bad message " + bad)
        }
      }
    }


    /* init */

    if (verbose) raw_messages += main_actor
    phase_changed += main_actor
    commands_changed += main_actor

    start(List(logic))
    Exn.release((main_actor !? Get_Startup).asInstanceOf[Exn.Result[Unit]])

    init_node(node_name, header, perspective, header_text)
    Exn.release((main_actor !? Get_Theory).asInstanceOf[Exn.Result[Unit]])
  }
}


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