[opentheory-users] package versions

[Ramana Kumar]

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

I foresee some confusion about the notion of "dependency". At the
moment, a package T1 depends on T2 if T1 is a union of packages
including T2. My initial incorrect guess was that T1 would depend on
T2 if T1 uses T2 to satisfying some of its assumptions. The analogy I
was making is that T1 needs T2 to be "installed" before T1 can be
"installed" and "run", that is, can prove its payload under minimal
assumptions. The vision I had was of packages (just the
concrete/specific ones) being built so as to depend only on the three
(or fewer if possible) axioms of HOL. Perhaps there should be another
concept and word for such a composition of packages...? Some packages
(especially ones whose assumptions are intended to be provided in many
different ways) would not fit under that concept, but several would.