Email Gateway (Aug 18 2022 at 19:11): Email Gateway (Aug 18 2022 at 19:11):From: Matthias Schmalz <Matthias.Schmalz@inf.ethz.ch>
Hi,
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.
I would appreciate any help on this very much!
Best,
Matthias
Email Gateway (Aug 18 2022 at 19:11):From: Makarius <makarius@sketis.net>
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
ex.scala
Email Gateway (Aug 18 2022 at 19:12):From: Matthias Schmalz <Matthias.Schmalz@inf.ethz.ch>
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.
Sure.
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).
Thanks for this example. It clarifies the situation a lot. So new output
by the Isabelle process is announced through the commands_changed bus
and the details on the new document state can be queried with the
snapshot method. I still have difficulties understanding what kind of
information a snapshot provides.
My current view is the following; feel free to correct any
misinterpretations:
The Document.Snapshot.command_state field indicates the response to a
given Isar command within the document node.
The Command.State.results field indicates what is usually displayed in
the Output Window of jEdit.
The Command.State.status field gives the annotations displayed with
jEdit's theory buffer.
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.
Synchronizing input and output is one of the main challenges in my
application.
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.
Sure.
We can discuss in further detail what your application really requires.
There is much more to say and I would appreciate to discuss this, but I
have a deadline for next weekend. I will come back to you after this.
Best,
Matthias
Email Gateway (Aug 18 2022 at 19:12):From: Makarius <makarius@sketis.net>
Document.Node identifies each document node in a semi-abstract manner.
It is indeed modeled after editor text buffers, can be used in other ways
as well. In the example, I've identified the fresh theory node by some
something like /dummy-42/Theory.thy
Document.Snapshot is the main access point of the totality of a collection
of document nodes in a document version, with semantic markup attached
(via the internal Command.State components). This is the main programming
interface to access results. It provides a defined point in space and
time of the ongoing process of continous checking of the sources. The key
operation is Snapshot.select_markup, but in the present example I have
uses more low-level status and results fields from individual command
states.
Command.State.results and Command.State.status are special cases of the
primary "markup" component of accumulated state information. In fact,
after Isabelle2011-1 the focus is shifting further to that general markup
tree, and result messages and status information might have to be
retrieved via Snapshot.select and some further variants of it.
Makarius
Email Gateway (Aug 18 2022 at 19:14):From: Holger Gast <gast@informatik.uni-tuebingen.de>
Hi Matthias,
since similar questions have popped up now and then on the list, I
have taken a closer look at your request on the basis of the implementation
of the I3P interface (see my web-page), because in principle
it already offers the required API to do "background proving".
To explain: as desirable for user interface software (see the MVC pattern),
the functionality of I3P is implemented entirely in a self-contained
infrastructure layer that is independent of the Netbeans interface
that happens to access that functionality now.
As a result, extended unit tests can be run against the functionality
(which have greatly helped in maintainance and debugging through
the different Isabelle releases of the past 2 years) and the bulk of the
software becomes portable (e.g. to Eclipse, as done prototypically
in a bachelor thesis in Tübingen). For a fuller motivation and
architecture description, see my UITP '10 paper.
In principle, the infrastructure layer thus enables running Isabelle
as a background prover directly, analogously to the existing unit tests
of the Isabelle driver module. At the core, the it provides a simple
execute/revoke model for commands (based on two methods of
CommandState), while I3P takes care of sending
appropriate Isabelle commands, interrupt signals, etc. as necessary.
(I3P even keeps sending INT until the command stops executing.)
However, the abstractions built into the architecture lead to some
boilerplate code (see the @Before methods of the tests) that is not nice
for the specific application.
I have now added a small IsabelleFacade class (in module APIAccess;
for Facade see Gamma et al. "Design Patterns", 1995),
which hopefully makes the procedure straightforward. The attachment
contains a demonstration of the following features:
execute theories / individual commands and
interrupt (explicit or automatic) looping commands after
some specified timeout.
bulk proof of several proof attempts in different theories,
with automatic switching between theories.
The SyncExec wrapper adapts the overall asynchronous
architecture of I3P to the requirement of synchronous processing
as necessary for testing or background proving. Its (straightforward)
implementation shows how to work with the signalling mechanisms
about changes in the processing state of some command in order to
wait for the completion of processing.
The new facade, as well as the most important API classes of the
infrastructure module IAPP, have JavaDoc explanations attached. Please
get back to me if I omitted some lazily, such that I can supply them lazily.
Hope this helps,
Holger
RunningTheoriesTest.java
Last updated: Apr 24 2024 at 01:07 UTC