[opentheory-users] package versions

[Ramana Kumar]

On Wed, Oct 12, 2011 at 10:54 PM, Joe Hurd <joe at gilith.com> wrote:
> 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

Great - thanks!

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

It seems like the check that the required theories are actually
installed isn't done right away, so first the article is processed
(possibly taking a long time) before failing because of the requires
line?

Also, after this happened to me and I had to install base, I then ran
into this problem:

FATAL ERROR: opentheory failed:
Error: package cl-0.5 is already staged for installation
package install from theory file failed

Even though cl does not appear in the list of installed packages. Now
I suppose I have to manually remove the "staged" installation by rm
-rf $OPENTHEORY/staging/cl-0.5 ?


On the topic of staging, after I produce an article by proof-logging,
would it be a good idea to immediately run
  opentheory info --article -o foo.art foo.art
to clean it up, or would that be redundant given that I might
eventually create a .thy file for it and process it somewhere along
the way with the tool?


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

I would rather hope that parameterized theories would become so common
as to be considered "the norm"... but I think your current default
treatment of "requires" is fine for now.

> I'll be interested in what you think of using the new feature.
I uploaded cl-0.5 just now with a requirement for base. Now it only
has 30 unsatisfied assumptions left... some (but not all) I think
should be in base, or rather, I need to think of a way to make my
articles depend on base only (+ maybe some compatibility packages)
without touching the HOL4 script files they are logged from.

But it seems like the "requires:" tags are being ignored in various
places. Like on the repo's package summary, or if I ask the tool:
  opentheory info --summary cl-0.5
it still lists things like |- T as one of the assumptions (but base
provides this).
It seems like the only time I got the list of the 30 actually
uncovered assumptions was when I issued the "install" command on my
.thy file.
I think it would be better if the requires tags made a difference to
the package summary...