[opentheory-users] package versions

[Joe Hurd]

Hi Ramana,

I just implemented this "requires" package information, and wrote a
brief description of the syntax here:

http://www.gilith.com/research/opentheory/theory.html
http://www.gilith.com/research/opentheory/example-1.0.html

What happens is when a theory file (*.thy) is installed, the
opentheory tool gets the "required" package names, looks up the latest
version of these packages that have been installed, and checks that
the theorems proved by these theory packages completely cover the
assumptions of the theory.

No "requires" tags is a warning, no version of these packages
installed is an error, and uncovered assumptions are listed as
warnings.

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

For a theory to be useful there must be some way to satisfy all of its
assumptions, so the author is asked to list a set of theories that
achieve this (sort of an existence proof that the theory can be used).

Right now warnings will be produced for parametrized theories and
axiom theories, but I think the feature is generally useful enough to
be enabled, and we can work out the right behavior for unusual
theories later.

> But it seems like there's no theory-semantics content to a "requires" tag?

Correct - it's just an extra check to help the theory author.

I'll be interested in what you think of using the new feature.

Cheers,

Joe