[opentheory-users] wishlist for the opentheory tool

[Joe Hurd]

Hi Ramana,

>>> Search for packages by term matching on the conclusions of theorems it exports
>>
>> Also a good idea, but harder to implement because the local
>> installation only knows this information about the packages that are
>> locally installed.
>
> perhaps on the website?
> package managers usually store enough about packages in various repos
> to be able to search by title and description... I think terms in the
> inputs and outputs of theories are at about the description level of
> theory packages... although I could understand perceiving them as at a
> level of more detail (since there may well be an English text
> description for a theory package too)

I think this is the right approach. I wanted to keep the locally
stored information to a minimum, so opentheory just locally stores the
name and checksum of the available packages on each repo. However, if
you want to search packages by description or theorem, then it's
reasonable to submit a request to the repo to do this on your behalf.
Which reduces the problem to...

> is it hard to implement for locally installed packages?

At this point I don't know: I should certainly consider this kind of
searchability when designing a machine readable format for theory
summaries.

Cheers,

Joe