[opentheory-users] package versions

[Joe Hurd]

Hi Ramana,

> In what sense are packages with the same name and different versions
> supposed to be similar?
> I would think that they are supposed to be accomplishing the same goal
> and later versions are just improvements.

Agreed.

> The opentheory tool currently seems to encourage treating them as
> unrelated packages.

This is mostly true - the OpenTheory toolset regards later versions as
obsoleting previous versions, which makes some difference:

 * The opentheory list command by default shows you the latest version
of theories

 * A repo won't let you upload a theory that obsoletes a theory from
another author (unless they consent).

> Specifically, I have a couple of suggestions about leaving version numbers off:
> For the opentheory install command, leaving the version number off a
> package name should just install the latest version of a package with
> that name.

Excellent suggestion - I will implement that.

> Similarly, within a package block in a theory file, a bare name should
> refer to the latest version.
> This would mean that a package's meaning would change over time even
> if the package stays the same, which might not be desirable.
> But it means a package depending on base wouldn't need to itself get a
> new version (with someone manually updating the theory file) every
> time base gets a new version.

Unfortunately, this would mean that it would be impossible to create a
theory summary with well-defined assumptions and theorems. As I
mention in another email

http://www.gilith.com/opentheory/mailing-list/2011-September/000152.html

the theory import mechanism is not used to check that the assumptions
of one theory are satisfied by the theorems of another, but rather for
a theory developer to craft a new theory as a composition of simpler
theories (usually authored by the same developer). To support this
crafting I think it's necessary for the theory developer to be able to
specify the precise version of the theories that are being composed.

> Other package management systems (e.g. for software) seem to work like
> this, although they sometimes allow a range of versions to be
> specified, e.g. package: base>=1.2 would mean anything after base-1.2
> should do.

Perhaps specifying a set of theories could also work, because the
theory developer could check at release time that whichever
combination of theories were composed the resulting theory would be
the same.

I think the broader point here is that in addition to the low-level
theory import mechanism for crafting individual theories, there should
be a higher-level mechanism to highlight which theories fit together.
Perhaps it could run on the repo, since the repo is in a position to
update it as later versions of theories are uploaded.

Cheers,

Joe