[opentheory-users] wishlist for the opentheory tool

[Joe Hurd]

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.

> 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).

> 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.

> 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

Cheers,

Joe