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
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
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 """)
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and