Re: [isabelle] Search in Isabelle



On Thu, 25 Mar 2010, grechukbogdan wrote:

Suggestion 1. The message like “The current goal could be solved directly with...” should appear not only after I formulate the existing result as a lemma, but also when I formulate it inside the proof, say after have. Ideally, something like this should work when the existing result appears as a subgoal in the proof, etc.

The goal-print-hook mechanism is essentially just a temporary workaround (since some years already). There is a fundamental bottle-neck in the synchronous interaction model of Proof General here, which is inherited from the plain tty model. I.e. there is just a single read-eval-print loop, and while the system is trying to find smart suggestions the user has to wait for it.

Activating this crude suggestion mechanism in more places would degrade system reactivity even further.


Suggestion 2: It should be a possibility to run Sledgehammer in the background automatically, every time when I formulate a lemma or “have” statement . If this is already possible, the suggestion is to make it more clear how to turn it on, because I cannot find the way to do this.

Same problem, even worse. Users certainly do not want to wait several seconds until they can continue typing.

The crude asynchronous mode of Sledgehammer is also just a temporary workaround.


Quite some time ago, I've started an effort to introduce true interaction into interactive theorem proving, by giving up the tty read-eval-print loop, and Proof General, heading towards a document-oriented editor model.

This is much easier said then done. There are many technical issues, part of them already solved. At least initially it was hard to find a replacement for the Emacs operating system (with its modest single-threaded editor). What has emerged already is this new Isabelle/Pure.jar Scala library for system programming, and a small demo application based on the powerful jEdit, which is a real editor, not an operating sytem like Emacs or Eclipse.

I hope to see some usuable asynchronous proof editor within the next few months. The asynchronous model will provide a natural playground for various "user agents" based on find_theorems, external ATPs etc. There is lots of implementation work still ahead of us -- as well as unlearning the way of thinking in terms of a TTY-loop.


Suggestion 4: There should be a simple way to see the any definition in Isabelle, even if I do not know in advance, is this a lemma, method, term, abbreviation, notation, or something else.

You cannot easily have a "whatis FOO" command that tells you about an uncategorized entity FOO -- it would violate the internal data abstraction of Isabelle tools and packages. But such a command would belong to the old TTY world anyway.

What works already is a universal markup mechanism that decorates all input and output of the system by formal references to defining and referencing locations etc. For example, looking at some bit of text like "SOME x. P x" that has been digested by the system at some point, you could click on the "SOME" or even the "." to refer to the formal entity behind it, say a constant definition with notation for concrete syntax.

Too bad there is still no user interface, or even just HTML browser to make use of this information emitted by Isabelle. The Proof General setup strips it all away -- the single LISP thread would choke on all that semantic information anyway.

Moreover, if you look at modern Isabelle documentation, it is all based on formal theories. Manuals such as isar-ref have further formal markup in the running text, say @{method_def induct} (defining position) or @{method_ref induct} (interesting referencing position), or @{method induct} (other reference). Right now this is only used to produce a traditional LaTeX index, but the pointing and clicking on formal entities as sketched above could be applied as well.

For example, lets say you look at some bits of theory somewhere in the library:

  lemma fixes n :: nat shows "P n" by (induct n) auto

To understand what "induct" is, you merely right-click and select from whatever manuals are presented there, you should quickly get to reference-manual style definitions of it, or some specially marked examples etc.


Isabelle already provides a good portion of such mechanisms internally, but the front-ends are still lacking. Something like two years ago I've started to engage myself into the Scala/JVM programming language, to get access to JVM based editor and browser technologies, without having to work with the crude oil industry stuff around Java. Thus the ML (and HOL) culture of Isabelle can be extended into the JVM, thanks to the smart guys from EPF Lausanne.


Stay tuned for more to come here soon.


If anybody wants to help me out, what I desparately need is:

  * A really good PDF browser for the JVM (as pure jar, no JNI crap);
    hyperlinks and copy-paste need to work properly.

  * A really good HTML browser in the same manner.  Presently I am using
    Lobo/Cobra, which is quite good, but also has some shortcomings.
    (I've tried Flying Saucer already.)

Of course, all of that needs to be Open Source.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.