Re: [isabelle] Interfacing with Isabelle



On Fri, 27 Feb 2009, Scott West wrote:

> > Well, your ML function does not have to terminate immediately.  The 
> > setup for Proof General for example takes over the tty and then reacts 
> > to further input.  All of this is very delicate to get right, though.  
> > Better try something based on the new process wrapper.
> 
> I've found the grammar for the Isabelle input syntax, but I have yet to 
> find one for the Isabelle output. Does one exist that you know of? It 
> seems this would be crucial for the creation of higher levels of control 
> on top of what Isabelle offers.

(1) Command syntax.

The grammars for Isabelle/Isar commands, methods, attributes etc. in the 
manual are only for end-users.  When building a system that operates on 
input source systematically, you cannot count on that.  First of all, 
maintaining consistency with such a huge specification is practically 
impossible (the manual itself is probably not 100% correct).  Secondly 
such a specification can never be complete, because user applications may 
introduce new language elements at any time (Isabelle/HOL is just an 
"application" in that sense, albeit a large one).

What interfaces can rely on is the outer token syntax and the 
categorisation of "command keywords" as produced by a particular logic 
session.  The editor side can then chop up the source into "command spans" 
and rely on the system reacting in a certain way, e.g. do a theory update 
as in 'definition' or start a proof as in 'theorem'.  A very basic ML 
example of this rough syntactic analysis is parse_spans in 
http://isabelle.in.tum.de/repos/isabelle/file/83c50c62cf23/src/Pure/Thy/thy_syntax.ML

At some later stage we will provide this kind of functionality on the 
Scala level as well, but it will be more flexible, operating on some kind 
of editor buffer model instead of doing batch-mode parsing.


(2) Message syntax.

Messages are merely packets of text sent to certain "output channels", 
e.g. writeln, warning, error. There are hooks for each channel, so the 
interface ML wrapper can do whatever it needs to do.  E.g. see 
Output.warning_fn and its redifinition in the various wrappers (use "grep 
-r" or hypersearch in jEdit to find the places).

Thus you get messages plus some message type information.  Apart from that 
there is usually extra markup within the body, e.g. when printing a term 
you get information about bound, free, schematic variables etc.  Proof 
General turns this into the well-known colour scheme for variables.  You 
can also inspect the markup in semi-human-readable form like this in Proof 
General:

  thm (test_markup) exE

The representation of markup in existing interfaces is quite adhoc -- no 
need to look into that.  The new Isabelle process wrapper (remember 
isabelle-process option -W) always uses (untyped) XML trees encoded in 
YXML transfer syntax (this format is explained in the Isabelle System 
manual).  When using the Scala wrapper around that, you do not have to 
care about the encoding, but get back the tree structure directly.

These trees are still uninterpreted.  We will probably add some kind of 
default rendering via CSS at some stage.


(3) Scala wrapper.

I have mentioned the Isabelle scala wrapper several times already.  Here 
is a simple example session (using the development snapshot of Isabelle, 
or a repository version after invoking "Admin/build jars"):

  $ isabelle scala
  scala> val p = new isabelle.IsabelleProcess("HOL")
  scala> p.command(""" theory A imports Main begin """)

  WRITELN [[theory A]]

  scala> p.command(""" theorem "A --> A" """)

  WRITELN [[proof (prove): step 0

goal (1 subgoal):
 1. A --> A]]

  scala> p.command(""" .. """)

  WRITELN [[theorem ?A --> ?A]]

  scala> p.command(""" end """)
  scala> p.close

  ...

In the transscript I have suppressed some of the more chatty messages.  
Here you have direct access to the most basic prover protocol: 
commands-in, messages-out.  But the protocol is not as simple as it seems, 
because commands can produces any number of messages in any order, 
potentially intermingled with messages from other commands that are 
running concurrently.  (Note that the prover "prompt" still used in Proof 
General no longer exists.)

Our next step is to wrap up the command/message protocol into a proper 
document model that maintains sources + command structure + message 
feedback as extra markup to the sources.


	Makarius





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