[isabelle-dev] NEWS: Dockable window "Find"

[Gerwin Klein]

On 09/08/2013, at 9:05 PM, Makarius <makarius at sketis.net> wrote:

> *** Prover IDE -- Isabelle/Scala/jEdit ***
>
> * Dockable window "Find" provides query operations for formal entities
> (GUI front-end to 'find_theorems' command).

This sounds cool, will try it out soon.


> Anyway, what is the purpose of the find_theorems rem_dups / with_dups option?  I have made a tooltip that says "Allow duplicates in result (faster for large theories)", although I am unsure if this is correct. The result with duplicates is quite different, i.e. not sorted according to the usual heuristics.
>
> Is this special "Duplicates" treatment still relevant?

Yes, it's still relevant. One of the uses of the command where duplicates are reported is to see how often the same theorem is proved under different names, which these are, and how to best consolidate them. It's usually used with narrow search parameters, so that the result lists tend to be small. It's less about the speed of the output (that may have been a consideration very early on, but not in the last years).


> Already for Isabelle2013 I've put some Par_List.map combinators in place, both for filter evaluation and pretty printing of the result.  Can anyone with access to secret benchmarks try how well this crunches on 8 or 16 cores?

I haven't noticed any marked difference in normal usage. At least on our theories the performance of find_theorems has been pretty satisfactory the last few years.

There have been issues with printing of large goal states in the past, and I'm not sure if they are fully sorted out yet, but as far as I can tell these are unrelated.

Cheers,
Gerwin


________________________________

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.