[opentheory-users] wishlist for the opentheory tool

[Ramana Kumar]

On Fri, Jan 14, 2011 at 7:00 PM, Joe Hurd <joe at gilith.com> wrote:
> Hi Ramana,
>
> Thanks for the feature requests: here are my thoughts on them.
>
>> List/search available repos (Is a repo identified by a URL?)
>
> The repos known to one particular installation of OpenTheory are
> listed in the ~/.opentheory/config file. It would make sense for the
> OpenTheory project home page to contain a list of all public repos.
>
>> Search for packages by name
>
> Good idea: I've been tossing around the idea of an "opentheory search"
> command for a while.
>
>> 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)

is it hard to implement for locally installed packages?

>
>> Option to print types in info --summary
>> Option to print arities of type operators in info --summary
>
> I could certainly add a flag to print this information, but in my
> experience these annotations make the output a lot less readable. Have
> you tried mousing over elements in the HTML package summary
>
> http://opentheory.gilith.com/opentheory/packages/base-1.0/base-1.0.html
>
> The information you ask for should magically pop up when you leave the
> mouse over an element for while (at least, it does on my Firefox
> browser).

Yeah the tooltips work - nice.
I think I mainly wanted the info for machine reading - for humans the
current output is fine (and the html is even better).

>
>> Machine readable version of info --summary output
>
> Good idea: in the future plans.
>
>> Option to disable "Show:" tags in info --summary
>
> Good idea.
>
>> Article file optimization. (Given an article file, write a new one
>> that has the same imports and exports but uses fewer virtual machine
>> instructions; optionally the instructions could be weighted by
>> "difficulty".)
>
> The opentheory tool already does this:
>
> opentheory info --article -o output.art input.art
>
> applies some heuristics (mainly sharing maximization) to compress
> input.art and writes the result to output.art.

Excellent!
I guess I should only think about further optimizations when I have
some slow examples to play with.

>
>> Somewhere to store a list like this of desired features (and issues
>> etc.) that can be publicly viewed and edited, i.e. bug tracker.
>
> This is trickier: I've been avoiding setting up accounts in the
> OpenTheory project, but allowing people to submit feature requests
> anonymously would invite spam. For now, I propose using the email list
> for this purpose: I'll try to fix bugs ASAP, and will maintain a list
> of feature requests at
>
> http://www.gilith.com/software/opentheory/requests.html

OK great.

>
> Cheers,
>
> Joe
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>