[isabelle-dev] Diagnostic commands in jedit?

[Makarius]

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