Email Gateway (Aug 18 2022 at 13:04): Email Gateway (Aug 18 2022 at 13:04):From: Scott West <scott.west@inf.ethz.ch>
Hello list!
Is there a standard, accepted, advised, or otherwise endorsed method of
interfacing with the Isabelle system? Currently I have a small program
which spawns a Isabelle TTY through the isatool, and communicates
through the standard handles.
I feel this may not be the best way for automated-interaction (I'm
trying to see if I can make a new interface). Is there some other way
that is recommended? I also tried just invoking isabelle, at which point
I became stymied by the documentation of the underlying ML (is there
some disjointedness between the documentation and the current release?).
Thanks in advance!
Regards,
Scott West
(PS, sorry if this is the third message that is received of this sort,
the list wasn't responding to my mails...)
Email Gateway (Aug 18 2022 at 13:04):From: Makarius <makarius@sketis.net>
On Wed, 25 Feb 2009, Scott West wrote:
Is there a standard, accepted, advised, or otherwise endorsed method of
interfacing with the Isabelle system? Currently I have a small program
which spawns a Isabelle TTY through the isatool, and communicates
through the standard handles.
Traditionally, the "standard" way to work with Isabelle under external
program control is rather primitive, see the "isabelle-process" command in
the system manual. Here you get access to the raw ML toplevel, and you
can pass ML expressions via the -e option. In principle this allows you
to do whatever you want, by invoking suitable ML things of your own
making. (Which is quite admittedly quite hard.)
A few such interaction wrappers have emerged in the past (notably for
Proof General), and made it into the official distribution, adding funny
options like -P -I -X to isabelle-process.
Starting with Isabelle2008 we have introduced one final wrapper
(isabelle-process option -W), which is meant to interface to a proper API
that lives in the JVM world. That JVM library is part of the official
Isabelle distribution, so user code does not need to fiddle with low-level
interaction protocols anymore (that is the basic plan).
In Isabelle2008 this extra layer is still Java/JVM, but we have already
left behind Java altogether in favour of Scala/JVM (which is the Next Big
Thing in programming language design, see http://www.scala-lang.org/).
There are still many things missing here; we have only started to make
actual use of Isabelle within the Scala/JVM world, using jEdit as editor
framework. Others have tried Netbeans with some success.
I feel this may not be the best way for automated-interaction (I'm
trying to see if I can make a new interface).
Can you be more specific what you are working on? Interacting with
interactive provers under program control is very hard to get right. I
have been involved in a couple of attempts so far, some succesful, many
failed.
I became stymied by the documentation of the underlying ML (is there
some disjointedness between the documentation and the current release?).
The manuals usually lag behind the real system a couple of years. The
newer manuals are at least formally checked against the system, meaning
that any references to ML entities, Isar commands, methods etc. correct.
For the forthcoming release the main reference manuals (isar-ref,
implementation, system) come in significantly updated and extended
versions. If your are interested, you may already peek at this version
via the repository
http://isabelle.in.tum.de/repos/isabelle/rev/351fc2f8493d (or later).
It is usually easier to peek at (fully tested) snapshots via
http://isabelle.in.tum.de/devel/ but that appears to be unmaintained right
now.
Makarius
Email Gateway (Aug 18 2022 at 13:04):From: Makarius <makarius@sketis.net>
On Thu, 26 Feb 2009, Scott West wrote:
Traditionally, the "standard" way to work with Isabelle under external
program control is rather primitive, see the "isabelle-process" command in
the system manual. Here you get access to the raw ML toplevel, and you
can pass ML expressions via the -e option. In principle this allows you
to do whatever you want, by invoking suitable ML things of your own
making. (Which is quite admittedly quite hard.)It sounds like this repeated invocation would make you constantly lose
the current proof state. Or can can this be avoided by
dumping/re-loading the heap every time? At the very least it sounds as
if it may have a high cost due to the repeated initializations of the
system?
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.
If your are interested, you may already peek at this version via the
repository http://isabelle.in.tum.de/repos/isabelle/rev/351fc2f8493d
(or later).I now have a development version compiled (I think... untested)
OK, maybe you want to subscribe to
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
which is the proper place to discuss things that are not in the official
release yet.
Also make sure to use polyml-5.2.1, say from
http://isabelle.in.tum.de/polyml-5.2.1/ -- otherwise threads will not
work, and these are required for any of the newer interaction models.
(Threads will also give you better multicore performance.)
Makarius
Email Gateway (Aug 18 2022 at 13:04):From: Makarius <makarius@sketis.net>
Maybe you are interested in the following presentations, which I have
given in Edinburgh 2007 and 2008, respectively:
Asynchronous processing of proof documents -- rethinking interactive
theorem proving
http://www4.in.tum.de/~wenzelm/papers/edinburgh2007.pdf
Interactive Proof Documents -- Theorem Provers for User Interfaces
http://www4.in.tum.de/~wenzelm/papers/edinburgh2008.pdf
Makarius
Email Gateway (Aug 18 2022 at 13:04):From: Scott West <scott.west@inf.ethz.ch>
Traditionally, the "standard" way to work with Isabelle under external
program control is rather primitive, see the "isabelle-process" command in
the system manual. Here you get access to the raw ML toplevel, and you
can pass ML expressions via the -e option. In principle this allows you
to do whatever you want, by invoking suitable ML things of your own
making. (Which is quite admittedly quite hard.)
It sounds like this repeated invocation would make you constantly lose the
current proof state. Or can can this be avoided by dumping/re-loading the heap
every time? At the very least it sounds as if it may have a high cost due to
the repeated initializations of the system?
Starting with Isabelle2008 we have introduced one final wrapper
(isabelle-process option -W), which is meant to interface to a proper API
that lives in the JVM world. That JVM library is part of the official
Isabelle distribution, so user code does not need to fiddle with low-level
interaction protocols anymore (that is the basic plan).In Isabelle2008 this extra layer is still Java/JVM, but we have already
left behind Java altogether in favour of Scala/JVM (which is the Next Big
Thing in programming language design, see http://www.scala-lang.org/).
I've actually used Scala a little before (and use Haskell quite a bit, so am
familiar with the functional style). I will give this a look.
success.
I feel this may not be the best way for automated-interaction (I'm
trying to see if I can make a new interface).Can you be more specific what you are working on? Interacting with
interactive provers under program control is very hard to get right. I
have been involved in a couple of attempts so far, some succesful, many
failed.
I can't be more specific, because I really don't know :). I am still in the
exploring stage right now, seeing what can be done and what the best way to do
it is. I will likely do another round of research on general theorem prover
interfaces and things like this if it proves needed (too busy right now).
I became stymied by the documentation of the underlying ML (is there
some disjointedness between the documentation and the current release?).The manuals usually lag behind the real system a couple of years. The
newer manuals are at least formally checked against the system, meaning
that any references to ML entities, Isar commands, methods etc. correct.For the forthcoming release the main reference manuals (isar-ref,
implementation, system) come in significantly updated and extended
versions. If your are interested, you may already peek at this version
via the repository
http://isabelle.in.tum.de/repos/isabelle/rev/351fc2f8493d (or later).
Ahhh, thanks for the tip! I now have a development version compiled (I
think... untested)
Regards,
Scott
Email Gateway (Aug 18 2022 at 13:05):From: Scott West <scott.west@inf.ethz.ch>
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.
Regards,
Scott
Email Gateway (Aug 18 2022 at 13:05):From: Makarius <makarius@sketis.net>
(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):
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
Last updated: May 03 2024 at 12:27 UTC