david.greenaway at nicta.com.au
Fri Sep 13 03:43:28 CEST 2013
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
For example, trying to view the current progress of the command:
map (fn x => (tracing (PolyML.makestring x);
OS.Process.sleep (seconds 0.1))) (1 upto 100)
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
Thanks again for all your hard work, and my apologies in advance if
I am raising issues that you are already aware of.
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.
More information about the isabelle-dev