[opentheory-users] package versions

[Ramana Kumar]

On Fri, Sep 23, 2011 at 1:16 AM, Joe Hurd <joe at gilith.com> wrote:
>> Yes. What do you mean by "run on the repo" though? I feel like this
>> information, of how certain packages are intended to be composed,
>> should be written down somewhere by the package maintainer.
>
> Here's what I had in mind, though I haven't implemented it yet.
>
> 1. The package author includes new tags in the theory file like so:
>
> requires: base
> requires: word16
>
> 2. At installation time, the opentheory tool checks that the theorems
> in the latest installed versions of the base and word16 theories
> satisfy the assumptions of the theory. If the check fails (or if
> either base or word16 are not installed), the theory is still
> installed but a warning is generated.
>
> 3. [This is the part that is run on the repo] The dependency is
> rechecked whenever new versions of base and word16 are installed, and
> the theory is marked as out-of-date if the check fails. Perhaps an
> automatic email is also dispatched to the package author to encourage
> them to update the package.
>
> What do you think of this proposed scheme?

I like it.

I have a couple of questions:

For step 2, which assumptions need to be satisfied? Would you just
check that at least one is satisfied? Or do you mean all should be? I
imagine it would be common to only satisfy a subset of the assumptions
using other packages, but I don't think it's worthwhile for a packager
to specify exactly which... although maybe they can do that to an
extent by the way they structure the blocks in a package file.

I presume the package summary page (and output from the info command,
etc.) will make use of the "requires:" tags to print summaries with
fewer assumptions and definitions, right?
But it seems like there's no theory-semantics content to a "requires" tag?