On Mon, 26 Sep 2011, Florian Haftmann wrote:
After using jedit a lot (by the way, I can really recommend it!), I ask
myself how diagnostic commands fit into its interaction model.
For purely diagnostic commands (thm, find_theorems) I think there is no
big deal.
More complicated are »diagnostic« commands with side effects, e.g.
sledgehammer or export_code. In the first case you can argue that,
after the side effect has been issued once, the sledgehammer command
will be replaced by a suitable metis call (maybe with comments giving
further hints). But what about export_code? It's purpose clearly is to
have a side effect. When to (re-)issue it then? Do we need a different
/ new concept there?
I am asking myself the same questions for quite some time. So far the
document model mainly covers "document constructors", according to some
half-forgotten Isar terminology. Diagnostic commands are only marginally
covered so far, since stateful "diagnostics" are conceptually bound to the
TTY loop.
This summer I've managed to sort out the issue for the 'pr' command at
least, which means that for the visible parts of the document there is an
asynchronous process to print goal states that end up as derived results
over existing document content. The next stage will be to generalize this
basic idea to further "asynchronous agents", which should subsume tools
like "auto quickcheck", "auto nitpick", "auto sledgehammer". (It needs a
bit more explicit management than plain 'pr', and I need to catch up with
the current state of all this in the still-existing TTY / Proof General
model).
Commands with genuine side-effects, typically on the file-system, are a
completely different issue. In the current Isabelle/jEdit PIDE model, the
prover is already detached from the file-system concerning theory sources.
The same will follow soon after the release for auxiliary files ('uses').
This means file-system access will be mainly limited to "value-oriented"
auxiliary files in tmp space (with unique id and disposed after a process
has consumed the content).
Things like code generation might be of the form of associating document
content that is generated by functional evaluation over the semantics of
the formal source text. Think of it as part of browser_info, not the src
tree. Part of the question is who or what is the target of generated
sources. One might consider funny ways to refer to "resources" of a
theory node, similar to the way 'uses' are located now within the
file-system wrt. the master directory, but without an actual physical
directory.
Makarius_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
