[isabelle-dev] Isabelle_12-Sep-2013

[David Greenaway]

Hi Makarius,

Thanks for your hard work for putting this together.

Most things I tried seemed to work out of the box on my 64-bit Linux
system, including sledgehammer, nitpick, etc.

I understand this is an integration test, and not a general release
candidate, but nevertheless I will write about a few small issues
I hit while playing with it:

  * While "auto try", "auto quickcheck" and "auto nitpick" seemed
    to work, I couldn't get "auto sledgehammer" to give me a response.
    The lemma I tried was:

        lemma "length xs > 0 ⟹ hd (rev xs) = last  xs"

    which sledgehammer is easily able to solve in less than two seconds
    on my machine.

  * It would be nice if symbol completion worked in the new "find"
    panel. Similarly, using the standard Isabelle font in the search box
    probably makes sense.

  * The new "find" panel doesn't report the number of matches; only
    the number displayed. For example, searching "True" displays:

      "displaying 40 theorem(s)"

    in the panel, while "find_theorems" reports:

      "found 222 theorem(s) (40 displayed):"

    which is perhaps more informative.

  * Key-bindings (or at least hooks for keybindings) would be helpful
    for the new find panel and sledgehammer panels. "isabelle-find" and
    "isabelle-sledgehammer" hooks exist, but don't place focus on the
    "search" box nor start a sledgehammer run.

  * The abbreviations described in the "README" panel for sub, sup
    and bold do not appear to work.

  * The new superscripts are confusing me. term "T\<^sub>a" parses,
    but "T\<^sup>a" does not. I must confess I don't understand the top
    NEWS entry describing what has changed.

Also, using a clean Isabelle install without local patches applied
reminded me of a number of longer standing issues:

  * The default "Error color" and "Running color" colours are very
    similar, making them hard to distinguish in the "theories" panel
    ("Is there an error in that theory, or is it just taking a long time
    to process?"). I personally modify my "Running color" to be
    a pleasant blue.

  * When opening a theory from the command line, it would be nice to
    have an option to automatically open dependent theory files without
    prompting. It is nice to type:

        isabelle jedit -l SomeLongRunningHeap FileWithManyDeps.thy

    go away for a coffee, and come back with everything ready to go.
    Currently, you have to click "yes" after the heap has built before
    Isabelle will start processing "FileWithManyDeps.thy".

  * The "output" panel has a habit of scrolling to the top each time
    the current output is appended to. It would be nice to preserve the
    user's position.

    For example, trying to view the current progress of the command:

      ML {*
          map (fn x => (tracing (PolyML.makestring x);
                    OS.Process.sleep (seconds 0.1))) (1 upto 100)
      *}

    is difficult.

I am, of course, happy to submit patches for review for any (or all) of
these problems if there is any indication that such patches would be
appreciated.

Thanks again for all your hard work, and my apologies in advance if
I am raising issues that you are already aware of.

Cheers,
David


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.