[opentheory-users] package versions

[Joe Hurd]

Hi Ramana,

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

Cheers,

Joe