Re: [isabelle] Indexed Sum/Product Operator

On 05/12/2012, at 6:58 AM, Makarius <makarius at> wrote:

> On Tue, 4 Dec 2012, Tobias Nipkow wrote:
>>> Sometimes these "aspects" are still missing or only approximative, but the coverage is increasing over time. So the need for separate diagnostic commands like find_consts is more and more diminished.
>> The interesting part of the functionality of find_consts is search by a given type (a bit like Hoogle, if you speak Haskell). How do you plan to replace that by tooltips and hyperlinks?
> This is just a different category of application: search over a "mathematical" library, and really good solutions to that are still missing.  (I am occasionally attending the MKM conference, where people are discussing that.)

I think that the combination of tooltips/hover links and the existing searches in find_theorems and find_consts is actually pretty good for searching our fact base (think back 10 years when grep was the power tool of choice).

Things can and should certainly be improved, but I wouldn't diminish one kind of tool over the other. Both have their place.

> In contrast, the application sketched in this thread, you have your formal (con)text where you presently work already.
> In the past query tools like find_theorems were often re-used to explore the local proof context, but this can be done more directly.

I don't agree, that's not how find_theorems gets used most often. It can be, and you're right that that part is better expressed by other methods in an IDE, but there is no way to express a context sensitive term pattern query mixed with negative naming constraints and further refinements in a simple click or tool tip.

We really want both tools. Simple diagnostic information should be easily and directly accessible, and more complex searches for type or term patterns need to be just as well supported. Maybe they can be integrated better (dialogs or similar, although I'm not a fan of these), but that's a different aspect.

Since we're on the IDE topic: one thing that we could make more use of from IDEs is intelligent context sensitive name completion (for constants, types, rules, proof methods, etc). Also, it would help if suggestions were sorted by frequency of use, e.g. "sledgehammer" should be suggested before "sledgehammer_params". Good IDEs excel at that.

I'm not suggesting to aim for any of this in the next release, but if we're looking to improve the user experience in the future, this might make a big difference.



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.

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