[opentheory-users] package versions

Ramana Kumar ramana.kumar at gmail.com
Sun Sep 18 20:30:01 UTC 2011

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

More information about the opentheory-users mailing list